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