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