Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mreexexlemd Structured version   Unicode version

Theorem mreexexlemd 14916
 Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 14920. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
mreexexlemd.1
mreexexlemd.2
mreexexlemd.3
mreexexlemd.4
mreexexlemd.5
mreexexlemd.6
mreexexlemd.7
Assertion
Ref Expression
mreexexlemd
Distinct variable groups:   ,   ,   ,   ,   ,,,,,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,,)   (,,,)   (,,,)   (,,,)   (,,,,)   (,)   (,)   (,)

Proof of Theorem mreexexlemd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mreexexlemd.6 . 2
2 mreexexlemd.4 . 2
3 mreexexlemd.5 . 2
4 mreexexlemd.7 . . . 4
5 simplr 754 . . . . . . . . . . 11
65breq1d 4463 . . . . . . . . . 10
7 simpr 461 . . . . . . . . . . 11
87breq1d 4463 . . . . . . . . . 10
96, 8orbi12d 709 . . . . . . . . 9
10 simpll 753 . . . . . . . . . . . 12
117, 10uneq12d 3664 . . . . . . . . . . 11
1211fveq2d 5876 . . . . . . . . . 10
135, 12sseq12d 3538 . . . . . . . . 9
145, 10uneq12d 3664 . . . . . . . . . 10
1514eleq1d 2536 . . . . . . . . 9
169, 13, 153anbi123d 1299 . . . . . . . 8
17 simpllr 758 . . . . . . . . . . 11
18 simpr 461 . . . . . . . . . . 11
1917, 18breq12d 4466 . . . . . . . . . 10
20 simplll 757 . . . . . . . . . . . 12
2118, 20uneq12d 3664 . . . . . . . . . . 11
2221eleq1d 2536 . . . . . . . . . 10
2319, 22anbi12d 710 . . . . . . . . 9
24 simplr 754 . . . . . . . . . 10
2524pweqd 4021 . . . . . . . . 9
2623, 25cbvrexdva2 3098 . . . . . . . 8
2716, 26imbi12d 320 . . . . . . 7
28 simpl 457 . . . . . . . . . 10
2928difeq2d 3627 . . . . . . . . 9
3029pweqd 4021 . . . . . . . 8
3130adantr 465 . . . . . . 7
3227, 31cbvraldva2 3097 . . . . . 6
3332, 30cbvraldva2 3097 . . . . 5
3433cbvalv 1996 . . . 4
354, 34sylib 196 . . 3
36 ssun2 3673 . . . . . 6
3736a1i 11 . . . . 5
383, 37ssexd 4600 . . . 4
39 mreexexlemd.2 . . . . . . . 8
40 mreexexlemd.1 . . . . . . . . . . 11
41 difexg 4601 . . . . . . . . . . 11
4240, 41syl 16 . . . . . . . . . 10
4342, 39ssexd 4600 . . . . . . . . 9
44 elpwg 4024 . . . . . . . . 9
4543, 44syl 16 . . . . . . . 8
4639, 45mpbird 232 . . . . . . 7
4746adantr 465 . . . . . 6
48 simpr 461 . . . . . . . 8
4948difeq2d 3627 . . . . . . 7
5049pweqd 4021 . . . . . 6
5147, 50eleqtrrd 2558 . . . . 5
52 mreexexlemd.3 . . . . . . . . 9
5342, 52ssexd 4600 . . . . . . . . . 10
54 elpwg 4024 . . . . . . . . . 10
5553, 54syl 16 . . . . . . . . 9
5652, 55mpbird 232 . . . . . . . 8
5756ad2antrr 725 . . . . . . 7
5850adantr 465 . . . . . . 7
5957, 58eleqtrrd 2558 . . . . . 6
60 simplr 754 . . . . . . . . . 10
6160breq1d 4463 . . . . . . . . 9
62 simpr 461 . . . . . . . . . 10
6362breq1d 4463 . . . . . . . . 9
6461, 63orbi12d 709 . . . . . . . 8
65 simpllr 758 . . . . . . . . . . 11
6662, 65uneq12d 3664 . . . . . . . . . 10
6766fveq2d 5876 . . . . . . . . 9
6860, 67sseq12d 3538 . . . . . . . 8
6960, 65uneq12d 3664 . . . . . . . . 9
7069eleq1d 2536 . . . . . . . 8
7164, 68, 703anbi123d 1299 . . . . . . 7
7262pweqd 4021 . . . . . . . 8
7360breq1d 4463 . . . . . . . . 9
7465uneq2d 3663 . . . . . . . . . 10
7574eleq1d 2536 . . . . . . . . 9
7673, 75anbi12d 710 . . . . . . . 8
7772, 76rexeqbidv 3078 . . . . . . 7
7871, 77imbi12d 320 . . . . . 6
7959, 78rspcdv 3222 . . . . 5
8051, 79rspcimdv 3220 . . . 4
8138, 80spcimdv 3200 . . 3
8235, 81mpd 15 . 2
831, 2, 3, 82mp3and 1327 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wo 368   wa 369   w3a 973  wal 1377   wceq 1379   wcel 1767  wral 2817  wrex 2818  cvv 3118   cdif 3478   cun 3479   wss 3481  cpw 4016   class class class wbr 4453  cfv 5594   cen 7525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-iota 5557  df-fv 5602 This theorem is referenced by:  mreexexlem4d  14919  mreexexd  14920
 Copyright terms: Public domain W3C validator