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

Theorem mreexexlemd 13874
 Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 13878. (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 733 . . . . . . . . . . 11
65breq1d 4225 . . . . . . . . . 10
7 simpr 449 . . . . . . . . . . 11
87breq1d 4225 . . . . . . . . . 10
96, 8orbi12d 692 . . . . . . . . 9
10 simpll 732 . . . . . . . . . . . 12
117, 10uneq12d 3504 . . . . . . . . . . 11
1211fveq2d 5735 . . . . . . . . . 10
135, 12sseq12d 3379 . . . . . . . . 9
145, 10uneq12d 3504 . . . . . . . . . 10
1514eleq1d 2504 . . . . . . . . 9
169, 13, 153anbi123d 1255 . . . . . . . 8
17 simpllr 737 . . . . . . . . . . 11
18 simpr 449 . . . . . . . . . . 11
1917, 18breq12d 4228 . . . . . . . . . 10
20 simplll 736 . . . . . . . . . . . 12
2118, 20uneq12d 3504 . . . . . . . . . . 11
2221eleq1d 2504 . . . . . . . . . 10
2319, 22anbi12d 693 . . . . . . . . 9
24 simplr 733 . . . . . . . . . 10
2524pweqd 3806 . . . . . . . . 9
2623, 25cbvrexdva2 2939 . . . . . . . 8
2716, 26imbi12d 313 . . . . . . 7
28 simpl 445 . . . . . . . . . 10
2928difeq2d 3467 . . . . . . . . 9
3029pweqd 3806 . . . . . . . 8
3130adantr 453 . . . . . . 7
3227, 31cbvraldva2 2938 . . . . . 6
3332, 30cbvraldva2 2938 . . . . 5
3433cbvalv 1985 . . . 4
354, 34sylib 190 . . 3
36 ssun2 3513 . . . . . 6
3736a1i 11 . . . . 5
383, 37ssexd 4353 . . . 4
39 mreexexlemd.2 . . . . . . . 8
40 mreexexlemd.1 . . . . . . . . . . 11
41 difexg 4354 . . . . . . . . . . 11
4240, 41syl 16 . . . . . . . . . 10
4342, 39ssexd 4353 . . . . . . . . 9
44 elpwg 3808 . . . . . . . . 9
4543, 44syl 16 . . . . . . . 8
4639, 45mpbird 225 . . . . . . 7
4746adantr 453 . . . . . 6
48 simpr 449 . . . . . . . 8
4948difeq2d 3467 . . . . . . 7
5049pweqd 3806 . . . . . 6
5147, 50eleqtrrd 2515 . . . . 5
52 mreexexlemd.3 . . . . . . . . 9
5342, 52ssexd 4353 . . . . . . . . . 10
54 elpwg 3808 . . . . . . . . . 10
5553, 54syl 16 . . . . . . . . 9
5652, 55mpbird 225 . . . . . . . 8
5756ad2antrr 708 . . . . . . 7
5850adantr 453 . . . . . . 7
5957, 58eleqtrrd 2515 . . . . . 6
60 simplr 733 . . . . . . . . . 10
6160breq1d 4225 . . . . . . . . 9
62 simpr 449 . . . . . . . . . 10
6362breq1d 4225 . . . . . . . . 9
6461, 63orbi12d 692 . . . . . . . 8
65 simpllr 737 . . . . . . . . . . 11
6662, 65uneq12d 3504 . . . . . . . . . 10
6766fveq2d 5735 . . . . . . . . 9
6860, 67sseq12d 3379 . . . . . . . 8
6960, 65uneq12d 3504 . . . . . . . . 9
7069eleq1d 2504 . . . . . . . 8
7164, 68, 703anbi123d 1255 . . . . . . 7
7262pweqd 3806 . . . . . . . 8
7360breq1d 4225 . . . . . . . . 9
7465uneq2d 3503 . . . . . . . . . 10
7574eleq1d 2504 . . . . . . . . 9
7673, 75anbi12d 693 . . . . . . . 8
7772, 76rexeqbidv 2919 . . . . . . 7
7871, 77imbi12d 313 . . . . . 6
7959, 78rspcdv 3057 . . . . 5
8051, 79rspcimdv 3055 . . . 4
8138, 80spcimdv 3035 . . 3
8235, 81mpd 15 . 2
831, 2, 3, 82mp3and 1283 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wo 359   wa 360   w3a 937  wal 1550   wceq 1653   wcel 1726  wral 2707  wrex 2708  cvv 2958   cdif 3319   cun 3320   wss 3322  cpw 3801   class class class wbr 4215  cfv 5457   cen 7109 This theorem is referenced by:  mreexexlem4d  13877  mreexexd  13878 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465
 Copyright terms: Public domain W3C validator