This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem aomclem6

Description: Lemma for dfac11 . Transfinite induction, close over z . (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem6.b 
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
aomclem6.c 
|- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
aomclem6.d 
|- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )
aomclem6.e 
|- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }
aomclem6.f 
|- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }
aomclem6.g 
|- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )
aomclem6.h 
|- H = recs ( ( z e. _V |-> G ) )
aomclem6.a 
|- ( ph -> A e. On )
aomclem6.y 
|- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
Assertion aomclem6 
|- ( ph -> ( H ` A ) We ( R1 ` A ) )

Proof

Step Hyp Ref Expression
1 aomclem6.b 
 |-  B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
2 aomclem6.c 
 |-  C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
3 aomclem6.d 
 |-  D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )
4 aomclem6.e 
 |-  E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }
5 aomclem6.f 
 |-  F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }
6 aomclem6.g 
 |-  G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )
7 aomclem6.h 
 |-  H = recs ( ( z e. _V |-> G ) )
8 aomclem6.a 
 |-  ( ph -> A e. On )
9 aomclem6.y 
 |-  ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
10 ssid 
 |-  A C_ A
11 8 adantr 
 |-  ( ( ph /\ A C_ A ) -> A e. On )
12 sseq1 
 |-  ( c = d -> ( c C_ A <-> d C_ A ) )
13 12 anbi2d 
 |-  ( c = d -> ( ( ph /\ c C_ A ) <-> ( ph /\ d C_ A ) ) )
14 fveq2 
 |-  ( c = d -> ( H ` c ) = ( H ` d ) )
15 fveq2 
 |-  ( c = d -> ( R1 ` c ) = ( R1 ` d ) )
16 14 15 weeq12d 
 |-  ( c = d -> ( ( H ` c ) We ( R1 ` c ) <-> ( H ` d ) We ( R1 ` d ) ) )
17 13 16 imbi12d 
 |-  ( c = d -> ( ( ( ph /\ c C_ A ) -> ( H ` c ) We ( R1 ` c ) ) <-> ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) ) )
18 sseq1 
 |-  ( c = A -> ( c C_ A <-> A C_ A ) )
19 18 anbi2d 
 |-  ( c = A -> ( ( ph /\ c C_ A ) <-> ( ph /\ A C_ A ) ) )
20 fveq2 
 |-  ( c = A -> ( H ` c ) = ( H ` A ) )
21 fveq2 
 |-  ( c = A -> ( R1 ` c ) = ( R1 ` A ) )
22 20 21 weeq12d 
 |-  ( c = A -> ( ( H ` c ) We ( R1 ` c ) <-> ( H ` A ) We ( R1 ` A ) ) )
23 19 22 imbi12d 
 |-  ( c = A -> ( ( ( ph /\ c C_ A ) -> ( H ` c ) We ( R1 ` c ) ) <-> ( ( ph /\ A C_ A ) -> ( H ` A ) We ( R1 ` A ) ) ) )
24 dmeq 
 |-  ( z = ( H |` c ) -> dom z = dom ( H |` c ) )
25 24 adantl 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> dom z = dom ( H |` c ) )
26 simpl1 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> c e. On )
27 onss 
 |-  ( c e. On -> c C_ On )
28 7 tfr1 
 |-  H Fn On
29 fnssres 
 |-  ( ( H Fn On /\ c C_ On ) -> ( H |` c ) Fn c )
30 28 29 mpan 
 |-  ( c C_ On -> ( H |` c ) Fn c )
31 fndm 
 |-  ( ( H |` c ) Fn c -> dom ( H |` c ) = c )
32 26 27 30 31 4syl 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> dom ( H |` c ) = c )
33 25 32 eqtrd 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> dom z = c )
34 33 26 eqeltrd 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> dom z e. On )
35 33 eleq2d 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> ( a e. dom z <-> a e. c ) )
36 35 biimpa 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> a e. c )
37 simpll2 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) )
38 simpl3l 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> ph )
39 38 adantr 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> ph )
40 onelss 
 |-  ( dom z e. On -> ( a e. dom z -> a C_ dom z ) )
41 34 40 syl 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> ( a e. dom z -> a C_ dom z ) )
42 41 imp 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> a C_ dom z )
43 simpl3r 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> c C_ A )
44 33 43 eqsstrd 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> dom z C_ A )
45 44 adantr 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> dom z C_ A )
46 42 45 sstrd 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> a C_ A )
47 sseq1 
 |-  ( d = a -> ( d C_ A <-> a C_ A ) )
48 47 anbi2d 
 |-  ( d = a -> ( ( ph /\ d C_ A ) <-> ( ph /\ a C_ A ) ) )
49 fveq2 
 |-  ( d = a -> ( H ` d ) = ( H ` a ) )
50 fveq2 
 |-  ( d = a -> ( R1 ` d ) = ( R1 ` a ) )
51 49 50 weeq12d 
 |-  ( d = a -> ( ( H ` d ) We ( R1 ` d ) <-> ( H ` a ) We ( R1 ` a ) ) )
52 48 51 imbi12d 
 |-  ( d = a -> ( ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) <-> ( ( ph /\ a C_ A ) -> ( H ` a ) We ( R1 ` a ) ) ) )
53 52 rspcva 
 |-  ( ( a e. c /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) ) -> ( ( ph /\ a C_ A ) -> ( H ` a ) We ( R1 ` a ) ) )
54 53 imp 
 |-  ( ( ( a e. c /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) ) /\ ( ph /\ a C_ A ) ) -> ( H ` a ) We ( R1 ` a ) )
55 36 37 39 46 54 syl22anc 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> ( H ` a ) We ( R1 ` a ) )
56 fveq1 
 |-  ( z = ( H |` c ) -> ( z ` a ) = ( ( H |` c ) ` a ) )
57 56 ad2antlr 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> ( z ` a ) = ( ( H |` c ) ` a ) )
58 fvres 
 |-  ( a e. c -> ( ( H |` c ) ` a ) = ( H ` a ) )
59 36 58 syl 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> ( ( H |` c ) ` a ) = ( H ` a ) )
60 57 59 eqtrd 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> ( z ` a ) = ( H ` a ) )
61 weeq1 
 |-  ( ( z ` a ) = ( H ` a ) -> ( ( z ` a ) We ( R1 ` a ) <-> ( H ` a ) We ( R1 ` a ) ) )
62 60 61 syl 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> ( ( z ` a ) We ( R1 ` a ) <-> ( H ` a ) We ( R1 ` a ) ) )
63 55 62 mpbird 
 |-  ( ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) /\ a e. dom z ) -> ( z ` a ) We ( R1 ` a ) )
64 63 ralrimiva 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
65 38 8 syl 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> A e. On )
66 38 9 syl 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
67 1 2 3 4 5 6 34 64 65 44 66 aomclem5 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> G We ( R1 ` dom z ) )
68 33 fveq2d 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> ( R1 ` dom z ) = ( R1 ` c ) )
69 weeq2 
 |-  ( ( R1 ` dom z ) = ( R1 ` c ) -> ( G We ( R1 ` dom z ) <-> G We ( R1 ` c ) ) )
70 68 69 syl 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> ( G We ( R1 ` dom z ) <-> G We ( R1 ` c ) ) )
71 67 70 mpbid 
 |-  ( ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) /\ z = ( H |` c ) ) -> G We ( R1 ` c ) )
72 71 ex 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> ( z = ( H |` c ) -> G We ( R1 ` c ) ) )
73 72 alrimiv 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> A. z ( z = ( H |` c ) -> G We ( R1 ` c ) ) )
74 nfv 
 |-  F/ d ( z = ( H |` c ) -> G We ( R1 ` c ) )
75 nfv 
 |-  F/ z d = ( H |` c )
76 nfsbc1v 
 |-  F/ z [. d / z ]. G We ( R1 ` c )
77 75 76 nfim 
 |-  F/ z ( d = ( H |` c ) -> [. d / z ]. G We ( R1 ` c ) )
78 eqeq1 
 |-  ( z = d -> ( z = ( H |` c ) <-> d = ( H |` c ) ) )
79 sbceq1a 
 |-  ( z = d -> ( G We ( R1 ` c ) <-> [. d / z ]. G We ( R1 ` c ) ) )
80 78 79 imbi12d 
 |-  ( z = d -> ( ( z = ( H |` c ) -> G We ( R1 ` c ) ) <-> ( d = ( H |` c ) -> [. d / z ]. G We ( R1 ` c ) ) ) )
81 74 77 80 cbvalv1 
 |-  ( A. z ( z = ( H |` c ) -> G We ( R1 ` c ) ) <-> A. d ( d = ( H |` c ) -> [. d / z ]. G We ( R1 ` c ) ) )
82 73 81 sylib 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> A. d ( d = ( H |` c ) -> [. d / z ]. G We ( R1 ` c ) ) )
83 nfsbc1v 
 |-  F/ d [. ( H |` c ) / d ]. [. d / z ]. G We ( R1 ` c )
84 fnfun 
 |-  ( H Fn On -> Fun H )
85 28 84 ax-mp 
 |-  Fun H
86 vex 
 |-  c e. _V
87 resfunexg 
 |-  ( ( Fun H /\ c e. _V ) -> ( H |` c ) e. _V )
88 85 86 87 mp2an 
 |-  ( H |` c ) e. _V
89 sbceq1a 
 |-  ( d = ( H |` c ) -> ( [. d / z ]. G We ( R1 ` c ) <-> [. ( H |` c ) / d ]. [. d / z ]. G We ( R1 ` c ) ) )
90 83 88 89 ceqsal 
 |-  ( A. d ( d = ( H |` c ) -> [. d / z ]. G We ( R1 ` c ) ) <-> [. ( H |` c ) / d ]. [. d / z ]. G We ( R1 ` c ) )
91 82 90 sylib 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> [. ( H |` c ) / d ]. [. d / z ]. G We ( R1 ` c ) )
92 sbccow 
 |-  ( [. ( H |` c ) / d ]. [. d / z ]. G We ( R1 ` c ) <-> [. ( H |` c ) / z ]. G We ( R1 ` c ) )
93 91 92 sylib 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> [. ( H |` c ) / z ]. G We ( R1 ` c ) )
94 nfcsb1v 
 |-  F/_ z [_ ( H |` c ) / z ]_ G
95 nfcv 
 |-  F/_ z ( R1 ` c )
96 94 95 nfwe 
 |-  F/ z [_ ( H |` c ) / z ]_ G We ( R1 ` c )
97 csbeq1a 
 |-  ( z = ( H |` c ) -> G = [_ ( H |` c ) / z ]_ G )
98 weeq1 
 |-  ( G = [_ ( H |` c ) / z ]_ G -> ( G We ( R1 ` c ) <-> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) ) )
99 97 98 syl 
 |-  ( z = ( H |` c ) -> ( G We ( R1 ` c ) <-> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) ) )
100 96 99 sbciegf 
 |-  ( ( H |` c ) e. _V -> ( [. ( H |` c ) / z ]. G We ( R1 ` c ) <-> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) ) )
101 88 100 ax-mp 
 |-  ( [. ( H |` c ) / z ]. G We ( R1 ` c ) <-> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) )
102 93 101 sylib 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) )
103 recsval 
 |-  ( c e. On -> ( recs ( ( z e. _V |-> G ) ) ` c ) = ( ( z e. _V |-> G ) ` ( recs ( ( z e. _V |-> G ) ) |` c ) ) )
104 7 fveq1i 
 |-  ( H ` c ) = ( recs ( ( z e. _V |-> G ) ) ` c )
105 fvex 
 |-  ( R1 ` dom z ) e. _V
106 105 105 xpex 
 |-  ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) e. _V
107 106 inex2 
 |-  ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) ) e. _V
108 6 107 eqeltri 
 |-  G e. _V
109 108 csbex 
 |-  [_ ( H |` c ) / z ]_ G e. _V
110 eqid 
 |-  ( z e. _V |-> G ) = ( z e. _V |-> G )
111 110 fvmpts 
 |-  ( ( ( H |` c ) e. _V /\ [_ ( H |` c ) / z ]_ G e. _V ) -> ( ( z e. _V |-> G ) ` ( H |` c ) ) = [_ ( H |` c ) / z ]_ G )
112 88 109 111 mp2an 
 |-  ( ( z e. _V |-> G ) ` ( H |` c ) ) = [_ ( H |` c ) / z ]_ G
113 7 reseq1i 
 |-  ( H |` c ) = ( recs ( ( z e. _V |-> G ) ) |` c )
114 113 fveq2i 
 |-  ( ( z e. _V |-> G ) ` ( H |` c ) ) = ( ( z e. _V |-> G ) ` ( recs ( ( z e. _V |-> G ) ) |` c ) )
115 112 114 eqtr3i 
 |-  [_ ( H |` c ) / z ]_ G = ( ( z e. _V |-> G ) ` ( recs ( ( z e. _V |-> G ) ) |` c ) )
116 103 104 115 3eqtr4g 
 |-  ( c e. On -> ( H ` c ) = [_ ( H |` c ) / z ]_ G )
117 weeq1 
 |-  ( ( H ` c ) = [_ ( H |` c ) / z ]_ G -> ( ( H ` c ) We ( R1 ` c ) <-> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) ) )
118 116 117 syl 
 |-  ( c e. On -> ( ( H ` c ) We ( R1 ` c ) <-> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) ) )
119 118 3ad2ant1 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> ( ( H ` c ) We ( R1 ` c ) <-> [_ ( H |` c ) / z ]_ G We ( R1 ` c ) ) )
120 102 119 mpbird 
 |-  ( ( c e. On /\ A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) /\ ( ph /\ c C_ A ) ) -> ( H ` c ) We ( R1 ` c ) )
121 120 3exp 
 |-  ( c e. On -> ( A. d e. c ( ( ph /\ d C_ A ) -> ( H ` d ) We ( R1 ` d ) ) -> ( ( ph /\ c C_ A ) -> ( H ` c ) We ( R1 ` c ) ) ) )
122 17 23 121 tfis3 
 |-  ( A e. On -> ( ( ph /\ A C_ A ) -> ( H ` A ) We ( R1 ` A ) ) )
123 11 122 mpcom 
 |-  ( ( ph /\ A C_ A ) -> ( H ` A ) We ( R1 ` A ) )
124 10 123 mpan2 
 |-  ( ph -> ( H ` A ) We ( R1 ` A ) )