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

Metamath Proof Explorer

Theorem dffi3

Description: The set of finite intersections can be "constructed" inductively by iterating binary intersection _om -many times. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis dffi3.1 
|- R = ( u e. _V |-> ran ( y e. u , z e. u |-> ( y i^i z ) ) )
Assertion dffi3 
|- ( A e. V -> ( fi ` A ) = U. ( rec ( R , A ) " _om ) )

Proof

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 eqabri 
 |-  ( 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 imbitrrdi 
 |-  ( ( 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 ) )