Step |
Hyp |
Ref |
Expression |
1 |
|
dffi3.1 |
|- R = ( u e. _V |-> ran ( y e. u , z e. u |-> ( y i^i z ) ) ) |
2 |
|
dffi2 |
|- ( A e. V -> ( fi ` A ) = |^| { x | ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) } ) |
3 |
|
fr0g |
|- ( A e. V -> ( ( rec ( R , A ) |` _om ) ` (/) ) = A ) |
4 |
|
frfnom |
|- ( rec ( R , A ) |` _om ) Fn _om |
5 |
|
peano1 |
|- (/) e. _om |
6 |
|
fnfvelrn |
|- ( ( ( rec ( R , A ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( rec ( R , A ) |` _om ) ` (/) ) e. ran ( rec ( R , A ) |` _om ) ) |
7 |
4 5 6
|
mp2an |
|- ( ( rec ( R , A ) |` _om ) ` (/) ) e. ran ( rec ( R , A ) |` _om ) |
8 |
3 7
|
eqeltrrdi |
|- ( A e. V -> A e. ran ( rec ( R , A ) |` _om ) ) |
9 |
|
elssuni |
|- ( A e. ran ( rec ( R , A ) |` _om ) -> A C_ U. ran ( rec ( R , A ) |` _om ) ) |
10 |
8 9
|
syl |
|- ( A e. V -> A C_ U. ran ( rec ( R , A ) |` _om ) ) |
11 |
|
reeanv |
|- ( E. m e. _om E. n e. _om ( c e. ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. ( ( rec ( R , A ) |` _om ) ` n ) ) <-> ( E. m e. _om c e. ( ( rec ( R , A ) |` _om ) ` m ) /\ E. n e. _om d e. ( ( rec ( R , A ) |` _om ) ` n ) ) ) |
12 |
|
eliun |
|- ( c e. U_ m e. _om ( ( rec ( R , A ) |` _om ) ` m ) <-> E. m e. _om c e. ( ( rec ( R , A ) |` _om ) ` m ) ) |
13 |
|
eliun |
|- ( d e. U_ n e. _om ( ( rec ( R , A ) |` _om ) ` n ) <-> E. n e. _om d e. ( ( rec ( R , A ) |` _om ) ` n ) ) |
14 |
12 13
|
anbi12i |
|- ( ( c e. U_ m e. _om ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. U_ n e. _om ( ( rec ( R , A ) |` _om ) ` n ) ) <-> ( E. m e. _om c e. ( ( rec ( R , A ) |` _om ) ` m ) /\ E. n e. _om d e. ( ( rec ( R , A ) |` _om ) ` n ) ) ) |
15 |
|
fniunfv |
|- ( ( rec ( R , A ) |` _om ) Fn _om -> U_ m e. _om ( ( rec ( R , A ) |` _om ) ` m ) = U. ran ( rec ( R , A ) |` _om ) ) |
16 |
15
|
eleq2d |
|- ( ( rec ( R , A ) |` _om ) Fn _om -> ( c e. U_ m e. _om ( ( rec ( R , A ) |` _om ) ` m ) <-> c e. U. ran ( rec ( R , A ) |` _om ) ) ) |
17 |
|
fniunfv |
|- ( ( rec ( R , A ) |` _om ) Fn _om -> U_ n e. _om ( ( rec ( R , A ) |` _om ) ` n ) = U. ran ( rec ( R , A ) |` _om ) ) |
18 |
17
|
eleq2d |
|- ( ( rec ( R , A ) |` _om ) Fn _om -> ( d e. U_ n e. _om ( ( rec ( R , A ) |` _om ) ` n ) <-> d e. U. ran ( rec ( R , A ) |` _om ) ) ) |
19 |
16 18
|
anbi12d |
|- ( ( rec ( R , A ) |` _om ) Fn _om -> ( ( c e. U_ m e. _om ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. U_ n e. _om ( ( rec ( R , A ) |` _om ) ` n ) ) <-> ( c e. U. ran ( rec ( R , A ) |` _om ) /\ d e. U. ran ( rec ( R , A ) |` _om ) ) ) ) |
20 |
4 19
|
ax-mp |
|- ( ( c e. U_ m e. _om ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. U_ n e. _om ( ( rec ( R , A ) |` _om ) ` n ) ) <-> ( c e. U. ran ( rec ( R , A ) |` _om ) /\ d e. U. ran ( rec ( R , A ) |` _om ) ) ) |
21 |
11 14 20
|
3bitr2i |
|- ( E. m e. _om E. n e. _om ( c e. ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. ( ( rec ( R , A ) |` _om ) ` n ) ) <-> ( c e. U. ran ( rec ( R , A ) |` _om ) /\ d e. U. ran ( rec ( R , A ) |` _om ) ) ) |
22 |
|
ordom |
|- Ord _om |
23 |
|
ordunel |
|- ( ( Ord _om /\ m e. _om /\ n e. _om ) -> ( m u. n ) e. _om ) |
24 |
22 23
|
mp3an1 |
|- ( ( m e. _om /\ n e. _om ) -> ( m u. n ) e. _om ) |
25 |
24
|
adantl |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( m u. n ) e. _om ) |
26 |
|
simprl |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> m e. _om ) |
27 |
25 26
|
jca |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( ( m u. n ) e. _om /\ m e. _om ) ) |
28 |
|
nnon |
|- ( y e. _om -> y e. On ) |
29 |
|
nnon |
|- ( x e. _om -> x e. On ) |
30 |
29
|
ad2antlr |
|- ( ( ( A e. V /\ x e. _om ) /\ y e. _om ) -> x e. On ) |
31 |
|
onsseleq |
|- ( ( y e. On /\ x e. On ) -> ( y C_ x <-> ( y e. x \/ y = x ) ) ) |
32 |
28 30 31
|
syl2an2 |
|- ( ( ( A e. V /\ x e. _om ) /\ y e. _om ) -> ( y C_ x <-> ( y e. x \/ y = x ) ) ) |
33 |
|
rzal |
|- ( x = (/) -> A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) |
34 |
33
|
biantrud |
|- ( x = (/) -> ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) <-> ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) /\ A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) ) |
35 |
|
fveq2 |
|- ( x = (/) -> ( ( rec ( R , A ) |` _om ) ` x ) = ( ( rec ( R , A ) |` _om ) ` (/) ) ) |
36 |
35
|
sseq1d |
|- ( x = (/) -> ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) <-> ( ( rec ( R , A ) |` _om ) ` (/) ) C_ ( fi ` A ) ) ) |
37 |
34 36
|
bitr3d |
|- ( x = (/) -> ( ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) /\ A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) <-> ( ( rec ( R , A ) |` _om ) ` (/) ) C_ ( fi ` A ) ) ) |
38 |
|
fveq2 |
|- ( x = n -> ( ( rec ( R , A ) |` _om ) ` x ) = ( ( rec ( R , A ) |` _om ) ` n ) ) |
39 |
38
|
sseq1d |
|- ( x = n -> ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) <-> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) ) |
40 |
38
|
sseq2d |
|- ( x = n -> ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) <-> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) ) ) |
41 |
40
|
raleqbi1dv |
|- ( x = n -> ( A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) <-> A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) ) ) |
42 |
39 41
|
anbi12d |
|- ( x = n -> ( ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) /\ A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) <-> ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) /\ A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) ) ) ) |
43 |
|
fveq2 |
|- ( x = suc n -> ( ( rec ( R , A ) |` _om ) ` x ) = ( ( rec ( R , A ) |` _om ) ` suc n ) ) |
44 |
43
|
sseq1d |
|- ( x = suc n -> ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) <-> ( ( rec ( R , A ) |` _om ) ` suc n ) C_ ( fi ` A ) ) ) |
45 |
43
|
sseq2d |
|- ( x = suc n -> ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) <-> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
46 |
45
|
raleqbi1dv |
|- ( x = suc n -> ( A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) <-> A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
47 |
44 46
|
anbi12d |
|- ( x = suc n -> ( ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) /\ A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) <-> ( ( ( rec ( R , A ) |` _om ) ` suc n ) C_ ( fi ` A ) /\ A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) ) |
48 |
|
ssfii |
|- ( A e. V -> A C_ ( fi ` A ) ) |
49 |
3 48
|
eqsstrd |
|- ( A e. V -> ( ( rec ( R , A ) |` _om ) ` (/) ) C_ ( fi ` A ) ) |
50 |
|
id |
|- ( x e. ( ( rec ( R , A ) |` _om ) ` n ) -> x e. ( ( rec ( R , A ) |` _om ) ` n ) ) |
51 |
|
eqidd |
|- ( x e. ( ( rec ( R , A ) |` _om ) ` n ) -> x = x ) |
52 |
|
ineq1 |
|- ( a = x -> ( a i^i b ) = ( x i^i b ) ) |
53 |
52
|
eqeq2d |
|- ( a = x -> ( x = ( a i^i b ) <-> x = ( x i^i b ) ) ) |
54 |
|
ineq2 |
|- ( b = x -> ( x i^i b ) = ( x i^i x ) ) |
55 |
|
inidm |
|- ( x i^i x ) = x |
56 |
54 55
|
eqtrdi |
|- ( b = x -> ( x i^i b ) = x ) |
57 |
56
|
eqeq2d |
|- ( b = x -> ( x = ( x i^i b ) <-> x = x ) ) |
58 |
53 57
|
rspc2ev |
|- ( ( x e. ( ( rec ( R , A ) |` _om ) ` n ) /\ x e. ( ( rec ( R , A ) |` _om ) ` n ) /\ x = x ) -> E. a e. ( ( rec ( R , A ) |` _om ) ` n ) E. b e. ( ( rec ( R , A ) |` _om ) ` n ) x = ( a i^i b ) ) |
59 |
50 50 51 58
|
syl3anc |
|- ( x e. ( ( rec ( R , A ) |` _om ) ` n ) -> E. a e. ( ( rec ( R , A ) |` _om ) ` n ) E. b e. ( ( rec ( R , A ) |` _om ) ` n ) x = ( a i^i b ) ) |
60 |
|
eqid |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) = ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) |
61 |
60
|
rnmpo |
|- ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) = { x | E. a e. ( ( rec ( R , A ) |` _om ) ` n ) E. b e. ( ( rec ( R , A ) |` _om ) ` n ) x = ( a i^i b ) } |
62 |
61
|
abeq2i |
|- ( x e. ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) <-> E. a e. ( ( rec ( R , A ) |` _om ) ` n ) E. b e. ( ( rec ( R , A ) |` _om ) ` n ) x = ( a i^i b ) ) |
63 |
59 62
|
sylibr |
|- ( x e. ( ( rec ( R , A ) |` _om ) ` n ) -> x e. ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) ) |
64 |
63
|
ssriv |
|- ( ( rec ( R , A ) |` _om ) ` n ) C_ ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) |
65 |
|
simpl |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> n e. _om ) |
66 |
|
fvex |
|- ( ( rec ( R , A ) |` _om ) ` n ) e. _V |
67 |
66
|
uniex |
|- U. ( ( rec ( R , A ) |` _om ) ` n ) e. _V |
68 |
67
|
pwex |
|- ~P U. ( ( rec ( R , A ) |` _om ) ` n ) e. _V |
69 |
|
inss1 |
|- ( a i^i b ) C_ a |
70 |
|
elssuni |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` n ) -> a C_ U. ( ( rec ( R , A ) |` _om ) ` n ) ) |
71 |
70
|
adantr |
|- ( ( a e. ( ( rec ( R , A ) |` _om ) ` n ) /\ b e. ( ( rec ( R , A ) |` _om ) ` n ) ) -> a C_ U. ( ( rec ( R , A ) |` _om ) ` n ) ) |
72 |
69 71
|
sstrid |
|- ( ( a e. ( ( rec ( R , A ) |` _om ) ` n ) /\ b e. ( ( rec ( R , A ) |` _om ) ` n ) ) -> ( a i^i b ) C_ U. ( ( rec ( R , A ) |` _om ) ` n ) ) |
73 |
|
vex |
|- a e. _V |
74 |
73
|
inex1 |
|- ( a i^i b ) e. _V |
75 |
74
|
elpw |
|- ( ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` n ) <-> ( a i^i b ) C_ U. ( ( rec ( R , A ) |` _om ) ` n ) ) |
76 |
72 75
|
sylibr |
|- ( ( a e. ( ( rec ( R , A ) |` _om ) ` n ) /\ b e. ( ( rec ( R , A ) |` _om ) ` n ) ) -> ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` n ) ) |
77 |
76
|
rgen2 |
|- A. a e. ( ( rec ( R , A ) |` _om ) ` n ) A. b e. ( ( rec ( R , A ) |` _om ) ` n ) ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` n ) |
78 |
60
|
fmpo |
|- ( A. a e. ( ( rec ( R , A ) |` _om ) ` n ) A. b e. ( ( rec ( R , A ) |` _om ) ` n ) ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` n ) <-> ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` n ) X. ( ( rec ( R , A ) |` _om ) ` n ) ) --> ~P U. ( ( rec ( R , A ) |` _om ) ` n ) ) |
79 |
77 78
|
mpbi |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` n ) X. ( ( rec ( R , A ) |` _om ) ` n ) ) --> ~P U. ( ( rec ( R , A ) |` _om ) ` n ) |
80 |
|
frn |
|- ( ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` n ) X. ( ( rec ( R , A ) |` _om ) ` n ) ) --> ~P U. ( ( rec ( R , A ) |` _om ) ` n ) -> ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) C_ ~P U. ( ( rec ( R , A ) |` _om ) ` n ) ) |
81 |
79 80
|
ax-mp |
|- ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) C_ ~P U. ( ( rec ( R , A ) |` _om ) ` n ) |
82 |
68 81
|
ssexi |
|- ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) e. _V |
83 |
|
nfcv |
|- F/_ v A |
84 |
|
nfcv |
|- F/_ v n |
85 |
|
nfcv |
|- F/_ v ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) |
86 |
|
mpoeq12 |
|- ( ( u = v /\ u = v ) -> ( y e. u , z e. u |-> ( y i^i z ) ) = ( y e. v , z e. v |-> ( y i^i z ) ) ) |
87 |
86
|
anidms |
|- ( u = v -> ( y e. u , z e. u |-> ( y i^i z ) ) = ( y e. v , z e. v |-> ( y i^i z ) ) ) |
88 |
|
ineq1 |
|- ( y = a -> ( y i^i z ) = ( a i^i z ) ) |
89 |
|
ineq2 |
|- ( z = b -> ( a i^i z ) = ( a i^i b ) ) |
90 |
88 89
|
cbvmpov |
|- ( y e. v , z e. v |-> ( y i^i z ) ) = ( a e. v , b e. v |-> ( a i^i b ) ) |
91 |
87 90
|
eqtrdi |
|- ( u = v -> ( y e. u , z e. u |-> ( y i^i z ) ) = ( a e. v , b e. v |-> ( a i^i b ) ) ) |
92 |
91
|
rneqd |
|- ( u = v -> ran ( y e. u , z e. u |-> ( y i^i z ) ) = ran ( a e. v , b e. v |-> ( a i^i b ) ) ) |
93 |
92
|
cbvmptv |
|- ( u e. _V |-> ran ( y e. u , z e. u |-> ( y i^i z ) ) ) = ( v e. _V |-> ran ( a e. v , b e. v |-> ( a i^i b ) ) ) |
94 |
1 93
|
eqtri |
|- R = ( v e. _V |-> ran ( a e. v , b e. v |-> ( a i^i b ) ) ) |
95 |
|
rdgeq1 |
|- ( R = ( v e. _V |-> ran ( a e. v , b e. v |-> ( a i^i b ) ) ) -> rec ( R , A ) = rec ( ( v e. _V |-> ran ( a e. v , b e. v |-> ( a i^i b ) ) ) , A ) ) |
96 |
94 95
|
ax-mp |
|- rec ( R , A ) = rec ( ( v e. _V |-> ran ( a e. v , b e. v |-> ( a i^i b ) ) ) , A ) |
97 |
96
|
reseq1i |
|- ( rec ( R , A ) |` _om ) = ( rec ( ( v e. _V |-> ran ( a e. v , b e. v |-> ( a i^i b ) ) ) , A ) |` _om ) |
98 |
|
mpoeq12 |
|- ( ( v = ( ( rec ( R , A ) |` _om ) ` n ) /\ v = ( ( rec ( R , A ) |` _om ) ` n ) ) -> ( a e. v , b e. v |-> ( a i^i b ) ) = ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) ) |
99 |
98
|
anidms |
|- ( v = ( ( rec ( R , A ) |` _om ) ` n ) -> ( a e. v , b e. v |-> ( a i^i b ) ) = ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) ) |
100 |
99
|
rneqd |
|- ( v = ( ( rec ( R , A ) |` _om ) ` n ) -> ran ( a e. v , b e. v |-> ( a i^i b ) ) = ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) ) |
101 |
83 84 85 97 100
|
frsucmpt |
|- ( ( n e. _om /\ ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) e. _V ) -> ( ( rec ( R , A ) |` _om ) ` suc n ) = ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) ) |
102 |
65 82 101
|
sylancl |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( ( rec ( R , A ) |` _om ) ` suc n ) = ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) ) |
103 |
64 102
|
sseqtrrid |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) |
104 |
|
sstr2 |
|- ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) -> ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
105 |
103 104
|
syl5com |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
106 |
105
|
ralimdv |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) -> A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
107 |
|
vex |
|- n e. _V |
108 |
|
fveq2 |
|- ( y = n -> ( ( rec ( R , A ) |` _om ) ` y ) = ( ( rec ( R , A ) |` _om ) ` n ) ) |
109 |
108
|
sseq1d |
|- ( y = n -> ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) <-> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
110 |
107 109
|
ralsn |
|- ( A. y e. { n } ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) <-> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) |
111 |
103 110
|
sylibr |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> A. y e. { n } ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) |
112 |
106 111
|
jctird |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) -> ( A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) /\ A. y e. { n } ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) ) |
113 |
|
df-suc |
|- suc n = ( n u. { n } ) |
114 |
113
|
raleqi |
|- ( A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) <-> A. y e. ( n u. { n } ) ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) |
115 |
|
ralunb |
|- ( A. y e. ( n u. { n } ) ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) <-> ( A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) /\ A. y e. { n } ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
116 |
114 115
|
bitri |
|- ( A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) <-> ( A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) /\ A. y e. { n } ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
117 |
112 116
|
syl6ibr |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) -> A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) |
118 |
|
fiin |
|- ( ( a e. ( fi ` A ) /\ b e. ( fi ` A ) ) -> ( a i^i b ) e. ( fi ` A ) ) |
119 |
118
|
rgen2 |
|- A. a e. ( fi ` A ) A. b e. ( fi ` A ) ( a i^i b ) e. ( fi ` A ) |
120 |
|
ss2ralv |
|- ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) -> ( A. a e. ( fi ` A ) A. b e. ( fi ` A ) ( a i^i b ) e. ( fi ` A ) -> A. a e. ( ( rec ( R , A ) |` _om ) ` n ) A. b e. ( ( rec ( R , A ) |` _om ) ` n ) ( a i^i b ) e. ( fi ` A ) ) ) |
121 |
119 120
|
mpi |
|- ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) -> A. a e. ( ( rec ( R , A ) |` _om ) ` n ) A. b e. ( ( rec ( R , A ) |` _om ) ` n ) ( a i^i b ) e. ( fi ` A ) ) |
122 |
60
|
fmpo |
|- ( A. a e. ( ( rec ( R , A ) |` _om ) ` n ) A. b e. ( ( rec ( R , A ) |` _om ) ` n ) ( a i^i b ) e. ( fi ` A ) <-> ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` n ) X. ( ( rec ( R , A ) |` _om ) ` n ) ) --> ( fi ` A ) ) |
123 |
121 122
|
sylib |
|- ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) -> ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` n ) X. ( ( rec ( R , A ) |` _om ) ` n ) ) --> ( fi ` A ) ) |
124 |
123
|
frnd |
|- ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) -> ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) C_ ( fi ` A ) ) |
125 |
124
|
adantl |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ran ( a e. ( ( rec ( R , A ) |` _om ) ` n ) , b e. ( ( rec ( R , A ) |` _om ) ` n ) |-> ( a i^i b ) ) C_ ( fi ` A ) ) |
126 |
102 125
|
eqsstrd |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( ( rec ( R , A ) |` _om ) ` suc n ) C_ ( fi ` A ) ) |
127 |
117 126
|
jctild |
|- ( ( n e. _om /\ ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) ) -> ( A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) -> ( ( ( rec ( R , A ) |` _om ) ` suc n ) C_ ( fi ` A ) /\ A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) ) |
128 |
127
|
expimpd |
|- ( n e. _om -> ( ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) /\ A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) ) -> ( ( ( rec ( R , A ) |` _om ) ` suc n ) C_ ( fi ` A ) /\ A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) ) |
129 |
128
|
a1d |
|- ( n e. _om -> ( A e. V -> ( ( ( ( rec ( R , A ) |` _om ) ` n ) C_ ( fi ` A ) /\ A. y e. n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` n ) ) -> ( ( ( rec ( R , A ) |` _om ) ` suc n ) C_ ( fi ` A ) /\ A. y e. suc n ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` suc n ) ) ) ) ) |
130 |
37 42 47 49 129
|
finds2 |
|- ( x e. _om -> ( A e. V -> ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) /\ A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) ) |
131 |
130
|
impcom |
|- ( ( A e. V /\ x e. _om ) -> ( ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) /\ A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
132 |
131
|
simprd |
|- ( ( A e. V /\ x e. _om ) -> A. y e. x ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) |
133 |
132
|
r19.21bi |
|- ( ( ( A e. V /\ x e. _om ) /\ y e. x ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) |
134 |
133
|
ex |
|- ( ( A e. V /\ x e. _om ) -> ( y e. x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
135 |
134
|
adantr |
|- ( ( ( A e. V /\ x e. _om ) /\ y e. _om ) -> ( y e. x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
136 |
|
fveq2 |
|- ( y = x -> ( ( rec ( R , A ) |` _om ) ` y ) = ( ( rec ( R , A ) |` _om ) ` x ) ) |
137 |
|
eqimss |
|- ( ( ( rec ( R , A ) |` _om ) ` y ) = ( ( rec ( R , A ) |` _om ) ` x ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) |
138 |
136 137
|
syl |
|- ( y = x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) |
139 |
138
|
a1i |
|- ( ( ( A e. V /\ x e. _om ) /\ y e. _om ) -> ( y = x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
140 |
135 139
|
jaod |
|- ( ( ( A e. V /\ x e. _om ) /\ y e. _om ) -> ( ( y e. x \/ y = x ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
141 |
32 140
|
sylbid |
|- ( ( ( A e. V /\ x e. _om ) /\ y e. _om ) -> ( y C_ x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
142 |
141
|
ralrimiva |
|- ( ( A e. V /\ x e. _om ) -> A. y e. _om ( y C_ x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
143 |
142
|
ralrimiva |
|- ( A e. V -> A. x e. _om A. y e. _om ( y C_ x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
144 |
143
|
adantr |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> A. x e. _om A. y e. _om ( y C_ x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) ) |
145 |
|
ssun1 |
|- m C_ ( m u. n ) |
146 |
145
|
a1i |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> m C_ ( m u. n ) ) |
147 |
|
sseq2 |
|- ( x = ( m u. n ) -> ( y C_ x <-> y C_ ( m u. n ) ) ) |
148 |
|
fveq2 |
|- ( x = ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` x ) = ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
149 |
148
|
sseq2d |
|- ( x = ( m u. n ) -> ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) <-> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) |
150 |
147 149
|
imbi12d |
|- ( x = ( m u. n ) -> ( ( y C_ x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) <-> ( y C_ ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) ) |
151 |
|
sseq1 |
|- ( y = m -> ( y C_ ( m u. n ) <-> m C_ ( m u. n ) ) ) |
152 |
|
fveq2 |
|- ( y = m -> ( ( rec ( R , A ) |` _om ) ` y ) = ( ( rec ( R , A ) |` _om ) ` m ) ) |
153 |
152
|
sseq1d |
|- ( y = m -> ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) <-> ( ( rec ( R , A ) |` _om ) ` m ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) |
154 |
151 153
|
imbi12d |
|- ( y = m -> ( ( y C_ ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) <-> ( m C_ ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` m ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) ) |
155 |
150 154
|
rspc2v |
|- ( ( ( m u. n ) e. _om /\ m e. _om ) -> ( A. x e. _om A. y e. _om ( y C_ x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) -> ( m C_ ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` m ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) ) |
156 |
27 144 146 155
|
syl3c |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( ( rec ( R , A ) |` _om ) ` m ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
157 |
156
|
sseld |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( c e. ( ( rec ( R , A ) |` _om ) ` m ) -> c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) |
158 |
|
simprr |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> n e. _om ) |
159 |
25 158
|
jca |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( ( m u. n ) e. _om /\ n e. _om ) ) |
160 |
|
ssun2 |
|- n C_ ( m u. n ) |
161 |
160
|
a1i |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> n C_ ( m u. n ) ) |
162 |
|
sseq1 |
|- ( y = n -> ( y C_ ( m u. n ) <-> n C_ ( m u. n ) ) ) |
163 |
108
|
sseq1d |
|- ( y = n -> ( ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) <-> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) |
164 |
162 163
|
imbi12d |
|- ( y = n -> ( ( y C_ ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) <-> ( n C_ ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) ) |
165 |
150 164
|
rspc2v |
|- ( ( ( m u. n ) e. _om /\ n e. _om ) -> ( A. x e. _om A. y e. _om ( y C_ x -> ( ( rec ( R , A ) |` _om ) ` y ) C_ ( ( rec ( R , A ) |` _om ) ` x ) ) -> ( n C_ ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) ) |
166 |
159 144 161 165
|
syl3c |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( ( rec ( R , A ) |` _om ) ` n ) C_ ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
167 |
166
|
sseld |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( d e. ( ( rec ( R , A ) |` _om ) ` n ) -> d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) |
168 |
24
|
ad2antlr |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( m u. n ) e. _om ) |
169 |
|
peano2 |
|- ( ( m u. n ) e. _om -> suc ( m u. n ) e. _om ) |
170 |
|
fveq2 |
|- ( x = suc ( m u. n ) -> ( ( rec ( R , A ) |` _om ) ` x ) = ( ( rec ( R , A ) |` _om ) ` suc ( m u. n ) ) ) |
171 |
170
|
ssiun2s |
|- ( suc ( m u. n ) e. _om -> ( ( rec ( R , A ) |` _om ) ` suc ( m u. n ) ) C_ U_ x e. _om ( ( rec ( R , A ) |` _om ) ` x ) ) |
172 |
168 169 171
|
3syl |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( ( rec ( R , A ) |` _om ) ` suc ( m u. n ) ) C_ U_ x e. _om ( ( rec ( R , A ) |` _om ) ` x ) ) |
173 |
|
simprl |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
174 |
|
simprr |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
175 |
|
eqidd |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( c i^i d ) = ( c i^i d ) ) |
176 |
|
ineq1 |
|- ( a = c -> ( a i^i b ) = ( c i^i b ) ) |
177 |
176
|
eqeq2d |
|- ( a = c -> ( ( c i^i d ) = ( a i^i b ) <-> ( c i^i d ) = ( c i^i b ) ) ) |
178 |
|
ineq2 |
|- ( b = d -> ( c i^i b ) = ( c i^i d ) ) |
179 |
178
|
eqeq2d |
|- ( b = d -> ( ( c i^i d ) = ( c i^i b ) <-> ( c i^i d ) = ( c i^i d ) ) ) |
180 |
177 179
|
rspc2ev |
|- ( ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ ( c i^i d ) = ( c i^i d ) ) -> E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ( c i^i d ) = ( a i^i b ) ) |
181 |
173 174 175 180
|
syl3anc |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ( c i^i d ) = ( a i^i b ) ) |
182 |
|
vex |
|- c e. _V |
183 |
182
|
inex1 |
|- ( c i^i d ) e. _V |
184 |
|
eqeq1 |
|- ( x = ( c i^i d ) -> ( x = ( a i^i b ) <-> ( c i^i d ) = ( a i^i b ) ) ) |
185 |
184
|
2rexbidv |
|- ( x = ( c i^i d ) -> ( E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) x = ( a i^i b ) <-> E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ( c i^i d ) = ( a i^i b ) ) ) |
186 |
183 185
|
elab |
|- ( ( c i^i d ) e. { x | E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) x = ( a i^i b ) } <-> E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ( c i^i d ) = ( a i^i b ) ) |
187 |
181 186
|
sylibr |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( c i^i d ) e. { x | E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) x = ( a i^i b ) } ) |
188 |
|
eqid |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) = ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) |
189 |
188
|
rnmpo |
|- ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) = { x | E. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) E. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) x = ( a i^i b ) } |
190 |
187 189
|
eleqtrrdi |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( c i^i d ) e. ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) ) |
191 |
|
fvex |
|- ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) e. _V |
192 |
191
|
uniex |
|- U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) e. _V |
193 |
192
|
pwex |
|- ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) e. _V |
194 |
|
elssuni |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) -> a C_ U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
195 |
69 194
|
sstrid |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) -> ( a i^i b ) C_ U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
196 |
74
|
elpw |
|- ( ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) <-> ( a i^i b ) C_ U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
197 |
195 196
|
sylibr |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) -> ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
198 |
197
|
adantr |
|- ( ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) -> ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
199 |
198
|
rgen2 |
|- A. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) A. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |
200 |
188
|
fmpo |
|- ( A. a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) A. b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ( a i^i b ) e. ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) <-> ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) X. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) --> ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
201 |
199 200
|
mpbi |
|- ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) X. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) --> ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |
202 |
|
frn |
|- ( ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) : ( ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) X. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) --> ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) -> ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) C_ ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) |
203 |
201 202
|
ax-mp |
|- ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) C_ ~P U. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |
204 |
193 203
|
ssexi |
|- ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) e. _V |
205 |
|
nfcv |
|- F/_ v ( m u. n ) |
206 |
|
nfcv |
|- F/_ v ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) |
207 |
|
mpoeq12 |
|- ( ( v = ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ v = ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) -> ( a e. v , b e. v |-> ( a i^i b ) ) = ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) ) |
208 |
207
|
anidms |
|- ( v = ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) -> ( a e. v , b e. v |-> ( a i^i b ) ) = ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) ) |
209 |
208
|
rneqd |
|- ( v = ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) -> ran ( a e. v , b e. v |-> ( a i^i b ) ) = ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) ) |
210 |
83 205 206 97 209
|
frsucmpt |
|- ( ( ( m u. n ) e. _om /\ ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) e. _V ) -> ( ( rec ( R , A ) |` _om ) ` suc ( m u. n ) ) = ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) ) |
211 |
168 204 210
|
sylancl |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( ( rec ( R , A ) |` _om ) ` suc ( m u. n ) ) = ran ( a e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) , b e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) |-> ( a i^i b ) ) ) |
212 |
190 211
|
eleqtrrd |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( c i^i d ) e. ( ( rec ( R , A ) |` _om ) ` suc ( m u. n ) ) ) |
213 |
172 212
|
sseldd |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( c i^i d ) e. U_ x e. _om ( ( rec ( R , A ) |` _om ) ` x ) ) |
214 |
|
fniunfv |
|- ( ( rec ( R , A ) |` _om ) Fn _om -> U_ x e. _om ( ( rec ( R , A ) |` _om ) ` x ) = U. ran ( rec ( R , A ) |` _om ) ) |
215 |
4 214
|
ax-mp |
|- U_ x e. _om ( ( rec ( R , A ) |` _om ) ` x ) = U. ran ( rec ( R , A ) |` _om ) |
216 |
213 215
|
eleqtrdi |
|- ( ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) /\ ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) ) -> ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) |
217 |
216
|
ex |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( ( c e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) /\ d e. ( ( rec ( R , A ) |` _om ) ` ( m u. n ) ) ) -> ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) |
218 |
157 167 217
|
syl2and |
|- ( ( A e. V /\ ( m e. _om /\ n e. _om ) ) -> ( ( c e. ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. ( ( rec ( R , A ) |` _om ) ` n ) ) -> ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) |
219 |
218
|
rexlimdvva |
|- ( A e. V -> ( E. m e. _om E. n e. _om ( c e. ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. ( ( rec ( R , A ) |` _om ) ` n ) ) -> ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) |
220 |
219
|
imp |
|- ( ( A e. V /\ E. m e. _om E. n e. _om ( c e. ( ( rec ( R , A ) |` _om ) ` m ) /\ d e. ( ( rec ( R , A ) |` _om ) ` n ) ) ) -> ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) |
221 |
21 220
|
sylan2br |
|- ( ( A e. V /\ ( c e. U. ran ( rec ( R , A ) |` _om ) /\ d e. U. ran ( rec ( R , A ) |` _om ) ) ) -> ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) |
222 |
221
|
ralrimivva |
|- ( A e. V -> A. c e. U. ran ( rec ( R , A ) |` _om ) A. d e. U. ran ( rec ( R , A ) |` _om ) ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) |
223 |
131
|
simpld |
|- ( ( A e. V /\ x e. _om ) -> ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) ) |
224 |
|
fvex |
|- ( fi ` A ) e. _V |
225 |
224
|
elpw2 |
|- ( ( ( rec ( R , A ) |` _om ) ` x ) e. ~P ( fi ` A ) <-> ( ( rec ( R , A ) |` _om ) ` x ) C_ ( fi ` A ) ) |
226 |
223 225
|
sylibr |
|- ( ( A e. V /\ x e. _om ) -> ( ( rec ( R , A ) |` _om ) ` x ) e. ~P ( fi ` A ) ) |
227 |
226
|
ralrimiva |
|- ( A e. V -> A. x e. _om ( ( rec ( R , A ) |` _om ) ` x ) e. ~P ( fi ` A ) ) |
228 |
|
fnfvrnss |
|- ( ( ( rec ( R , A ) |` _om ) Fn _om /\ A. x e. _om ( ( rec ( R , A ) |` _om ) ` x ) e. ~P ( fi ` A ) ) -> ran ( rec ( R , A ) |` _om ) C_ ~P ( fi ` A ) ) |
229 |
4 227 228
|
sylancr |
|- ( A e. V -> ran ( rec ( R , A ) |` _om ) C_ ~P ( fi ` A ) ) |
230 |
|
sspwuni |
|- ( ran ( rec ( R , A ) |` _om ) C_ ~P ( fi ` A ) <-> U. ran ( rec ( R , A ) |` _om ) C_ ( fi ` A ) ) |
231 |
229 230
|
sylib |
|- ( A e. V -> U. ran ( rec ( R , A ) |` _om ) C_ ( fi ` A ) ) |
232 |
|
ssexg |
|- ( ( U. ran ( rec ( R , A ) |` _om ) C_ ( fi ` A ) /\ ( fi ` A ) e. _V ) -> U. ran ( rec ( R , A ) |` _om ) e. _V ) |
233 |
231 224 232
|
sylancl |
|- ( A e. V -> U. ran ( rec ( R , A ) |` _om ) e. _V ) |
234 |
|
sseq2 |
|- ( x = U. ran ( rec ( R , A ) |` _om ) -> ( A C_ x <-> A C_ U. ran ( rec ( R , A ) |` _om ) ) ) |
235 |
|
eleq2 |
|- ( x = U. ran ( rec ( R , A ) |` _om ) -> ( ( c i^i d ) e. x <-> ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) |
236 |
235
|
raleqbi1dv |
|- ( x = U. ran ( rec ( R , A ) |` _om ) -> ( A. d e. x ( c i^i d ) e. x <-> A. d e. U. ran ( rec ( R , A ) |` _om ) ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) |
237 |
236
|
raleqbi1dv |
|- ( x = U. ran ( rec ( R , A ) |` _om ) -> ( A. c e. x A. d e. x ( c i^i d ) e. x <-> A. c e. U. ran ( rec ( R , A ) |` _om ) A. d e. U. ran ( rec ( R , A ) |` _om ) ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) |
238 |
234 237
|
anbi12d |
|- ( x = U. ran ( rec ( R , A ) |` _om ) -> ( ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) <-> ( A C_ U. ran ( rec ( R , A ) |` _om ) /\ A. c e. U. ran ( rec ( R , A ) |` _om ) A. d e. U. ran ( rec ( R , A ) |` _om ) ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) ) |
239 |
238
|
elabg |
|- ( U. ran ( rec ( R , A ) |` _om ) e. _V -> ( U. ran ( rec ( R , A ) |` _om ) e. { x | ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) } <-> ( A C_ U. ran ( rec ( R , A ) |` _om ) /\ A. c e. U. ran ( rec ( R , A ) |` _om ) A. d e. U. ran ( rec ( R , A ) |` _om ) ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) ) |
240 |
233 239
|
syl |
|- ( A e. V -> ( U. ran ( rec ( R , A ) |` _om ) e. { x | ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) } <-> ( A C_ U. ran ( rec ( R , A ) |` _om ) /\ A. c e. U. ran ( rec ( R , A ) |` _om ) A. d e. U. ran ( rec ( R , A ) |` _om ) ( c i^i d ) e. U. ran ( rec ( R , A ) |` _om ) ) ) ) |
241 |
10 222 240
|
mpbir2and |
|- ( A e. V -> U. ran ( rec ( R , A ) |` _om ) e. { x | ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) } ) |
242 |
|
intss1 |
|- ( U. ran ( rec ( R , A ) |` _om ) e. { x | ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) } -> |^| { x | ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) } C_ U. ran ( rec ( R , A ) |` _om ) ) |
243 |
241 242
|
syl |
|- ( A e. V -> |^| { x | ( A C_ x /\ A. c e. x A. d e. x ( c i^i d ) e. x ) } C_ U. ran ( rec ( R , A ) |` _om ) ) |
244 |
2 243
|
eqsstrd |
|- ( A e. V -> ( fi ` A ) C_ U. ran ( rec ( R , A ) |` _om ) ) |
245 |
244 231
|
eqssd |
|- ( A e. V -> ( fi ` A ) = U. ran ( rec ( R , A ) |` _om ) ) |
246 |
|
df-ima |
|- ( rec ( R , A ) " _om ) = ran ( rec ( R , A ) |` _om ) |
247 |
246
|
unieqi |
|- U. ( rec ( R , A ) " _om ) = U. ran ( rec ( R , A ) |` _om ) |
248 |
245 247
|
eqtr4di |
|- ( A e. V -> ( fi ` A ) = U. ( rec ( R , A ) " _om ) ) |