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 ) )