Metamath Proof Explorer


Theorem mreexexlemd

Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexexlemd.1 φ X J
mreexexlemd.2 φ F X H
mreexexlemd.3 φ G X H
mreexexlemd.4 φ F N G H
mreexexlemd.5 φ F H I
mreexexlemd.6 φ F K G K
mreexexlemd.7 φ t u 𝒫 X t v 𝒫 X t u K v K u N v t u t I i 𝒫 v u i i t I
Assertion mreexexlemd φ j 𝒫 G F j j H I

Proof

Step Hyp Ref Expression
1 mreexexlemd.1 φ X J
2 mreexexlemd.2 φ F X H
3 mreexexlemd.3 φ G X H
4 mreexexlemd.4 φ F N G H
5 mreexexlemd.5 φ F H I
6 mreexexlemd.6 φ F K G K
7 mreexexlemd.7 φ t u 𝒫 X t v 𝒫 X t u K v K u N v t u t I i 𝒫 v u i i t I
8 simplr t = h u = f v = g u = f
9 8 breq1d t = h u = f v = g u K f K
10 simpr t = h u = f v = g v = g
11 10 breq1d t = h u = f v = g v K g K
12 9 11 orbi12d t = h u = f v = g u K v K f K g K
13 simpll t = h u = f v = g t = h
14 10 13 uneq12d t = h u = f v = g v t = g h
15 14 fveq2d t = h u = f v = g N v t = N g h
16 8 15 sseq12d t = h u = f v = g u N v t f N g h
17 8 13 uneq12d t = h u = f v = g u t = f h
18 17 eleq1d t = h u = f v = g u t I f h I
19 12 16 18 3anbi123d t = h u = f v = g u K v K u N v t u t I f K g K f N g h f h I
20 simpllr t = h u = f v = g i = j u = f
21 simpr t = h u = f v = g i = j i = j
22 20 21 breq12d t = h u = f v = g i = j u i f j
23 simplll t = h u = f v = g i = j t = h
24 21 23 uneq12d t = h u = f v = g i = j i t = j h
25 24 eleq1d t = h u = f v = g i = j i t I j h I
26 22 25 anbi12d t = h u = f v = g i = j u i i t I f j j h I
27 simplr t = h u = f v = g i = j v = g
28 27 pweqd t = h u = f v = g i = j 𝒫 v = 𝒫 g
29 26 28 cbvrexdva2 t = h u = f v = g i 𝒫 v u i i t I j 𝒫 g f j j h I
30 19 29 imbi12d t = h u = f v = g u K v K u N v t u t I i 𝒫 v u i i t I f K g K f N g h f h I j 𝒫 g f j j h I
31 simpl t = h u = f t = h
32 31 difeq2d t = h u = f X t = X h
33 32 pweqd t = h u = f 𝒫 X t = 𝒫 X h
34 33 adantr t = h u = f v = g 𝒫 X t = 𝒫 X h
35 30 34 cbvraldva2 t = h u = f v 𝒫 X t u K v K u N v t u t I i 𝒫 v u i i t I g 𝒫 X h f K g K f N g h f h I j 𝒫 g f j j h I
36 35 33 cbvraldva2 t = h u 𝒫 X t v 𝒫 X t u K v K u N v t u t I i 𝒫 v u i i t I f 𝒫 X h g 𝒫 X h f K g K f N g h f h I j 𝒫 g f j j h I
37 36 cbvalvw t u 𝒫 X t v 𝒫 X t u K v K u N v t u t I i 𝒫 v u i i t I h f 𝒫 X h g 𝒫 X h f K g K f N g h f h I j 𝒫 g f j j h I
38 7 37 sylib φ h f 𝒫 X h g 𝒫 X h f K g K f N g h f h I j 𝒫 g f j j h I
39 ssun2 H F H
40 39 a1i φ H F H
41 5 40 ssexd φ H V
42 1 difexd φ X H V
43 42 2 sselpwd φ F 𝒫 X H
44 43 adantr φ h = H F 𝒫 X H
45 simpr φ h = H h = H
46 45 difeq2d φ h = H X h = X H
47 46 pweqd φ h = H 𝒫 X h = 𝒫 X H
48 44 47 eleqtrrd φ h = H F 𝒫 X h
49 42 3 sselpwd φ G 𝒫 X H
50 49 ad2antrr φ h = H f = F G 𝒫 X H
51 47 adantr φ h = H f = F 𝒫 X h = 𝒫 X H
52 50 51 eleqtrrd φ h = H f = F G 𝒫 X h
53 simplr φ h = H f = F g = G f = F
54 53 breq1d φ h = H f = F g = G f K F K
55 simpr φ h = H f = F g = G g = G
56 55 breq1d φ h = H f = F g = G g K G K
57 54 56 orbi12d φ h = H f = F g = G f K g K F K G K
58 simpllr φ h = H f = F g = G h = H
59 55 58 uneq12d φ h = H f = F g = G g h = G H
60 59 fveq2d φ h = H f = F g = G N g h = N G H
61 53 60 sseq12d φ h = H f = F g = G f N g h F N G H
62 53 58 uneq12d φ h = H f = F g = G f h = F H
63 62 eleq1d φ h = H f = F g = G f h I F H I
64 57 61 63 3anbi123d φ h = H f = F g = G f K g K f N g h f h I F K G K F N G H F H I
65 55 pweqd φ h = H f = F g = G 𝒫 g = 𝒫 G
66 53 breq1d φ h = H f = F g = G f j F j
67 58 uneq2d φ h = H f = F g = G j h = j H
68 67 eleq1d φ h = H f = F g = G j h I j H I
69 66 68 anbi12d φ h = H f = F g = G f j j h I F j j H I
70 65 69 rexeqbidv φ h = H f = F g = G j 𝒫 g f j j h I j 𝒫 G F j j H I
71 64 70 imbi12d φ h = H f = F g = G f K g K f N g h f h I j 𝒫 g f j j h I F K G K F N G H F H I j 𝒫 G F j j H I
72 52 71 rspcdv φ h = H f = F g 𝒫 X h f K g K f N g h f h I j 𝒫 g f j j h I F K G K F N G H F H I j 𝒫 G F j j H I
73 48 72 rspcimdv φ h = H f 𝒫 X h g 𝒫 X h f K g K f N g h f h I j 𝒫 g f j j h I F K G K F N G H F H I j 𝒫 G F j j H I
74 41 73 spcimdv φ h f 𝒫 X h g 𝒫 X h f K g K f N g h f h I j 𝒫 g f j j h I F K G K F N G H F H I j 𝒫 G F j j H I
75 38 74 mpd φ F K G K F N G H F H I j 𝒫 G F j j H I
76 6 4 5 75 mp3and φ j 𝒫 G F j j H I