Metamath Proof Explorer

Theorem axdc2lem

Description: Lemma for axdc2 . We construct a relation R based on F such that x R y iff y e. ( Fx ) , and show that the "function" described by ax-dc can be restricted so that it is a real function (since the stated properties only show that it is the superset of a function). (Contributed by Mario Carneiro, 25-Jan-2013) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses axdc2lem.1 
|- A e. _V
axdc2lem.2 
|- R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
axdc2lem.3 
|- G = ( x e. _om |-> ( h ` x ) )
Assertion axdc2lem 
|- ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc2lem.1 
 |-  A e. _V
2 axdc2lem.2 
 |-  R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
3 axdc2lem.3 
 |-  G = ( x e. _om |-> ( h ` x ) )
4 2 dmeqi 
 |-  dom R = dom { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
5 19.42v 
 |-  ( E. y ( x e. A /\ y e. ( F ` x ) ) <-> ( x e. A /\ E. y y e. ( F ` x ) ) )
6 5 abbii 
 |-  { x | E. y ( x e. A /\ y e. ( F ` x ) ) } = { x | ( x e. A /\ E. y y e. ( F ` x ) ) }
7 dmopab 
 |-  dom { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } = { x | E. y ( x e. A /\ y e. ( F ` x ) ) }
8 df-rab 
 |-  { x e. A | E. y y e. ( F ` x ) } = { x | ( x e. A /\ E. y y e. ( F ` x ) ) }
9 6 7 8 3eqtr4i 
 |-  dom { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } = { x e. A | E. y y e. ( F ` x ) }
10 4 9 eqtri 
 |-  dom R = { x e. A | E. y y e. ( F ` x ) }
11 ffvelcdm 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. A ) -> ( F ` x ) e. ( ~P A \ { (/) } ) )
12 eldifsni 
 |-  ( ( F ` x ) e. ( ~P A \ { (/) } ) -> ( F ` x ) =/= (/) )
13 n0 
 |-  ( ( F ` x ) =/= (/) <-> E. y y e. ( F ` x ) )
14 12 13 sylib 
 |-  ( ( F ` x ) e. ( ~P A \ { (/) } ) -> E. y y e. ( F ` x ) )
15 11 14 syl 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. A ) -> E. y y e. ( F ` x ) )
16 15 ralrimiva 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> A. x e. A E. y y e. ( F ` x ) )
17 rabid2 
 |-  ( A = { x e. A | E. y y e. ( F ` x ) } <-> A. x e. A E. y y e. ( F ` x ) )
18 16 17 sylibr 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> A = { x e. A | E. y y e. ( F ` x ) } )
19 10 18 eqtr4id 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> dom R = A )
20 19 neeq1d 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( dom R =/= (/) <-> A =/= (/) ) )
21 20 biimparc 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> dom R =/= (/) )
22 eldifi 
 |-  ( ( F ` x ) e. ( ~P A \ { (/) } ) -> ( F ` x ) e. ~P A )
23 elelpwi 
 |-  ( ( y e. ( F ` x ) /\ ( F ` x ) e. ~P A ) -> y e. A )
24 23 expcom 
 |-  ( ( F ` x ) e. ~P A -> ( y e. ( F ` x ) -> y e. A ) )
25 11 22 24 3syl 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. A ) -> ( y e. ( F ` x ) -> y e. A ) )
26 25 expimpd 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( ( x e. A /\ y e. ( F ` x ) ) -> y e. A ) )
27 26 exlimdv 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( E. x ( x e. A /\ y e. ( F ` x ) ) -> y e. A ) )
28 27 alrimiv 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> A. y ( E. x ( x e. A /\ y e. ( F ` x ) ) -> y e. A ) )
29 2 rneqi 
 |-  ran R = ran { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
30 rnopab 
 |-  ran { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } = { y | E. x ( x e. A /\ y e. ( F ` x ) ) }
31 29 30 eqtri 
 |-  ran R = { y | E. x ( x e. A /\ y e. ( F ` x ) ) }
32 31 sseq1i 
 |-  ( ran R C_ A <-> { y | E. x ( x e. A /\ y e. ( F ` x ) ) } C_ A )
33 abss 
 |-  ( { y | E. x ( x e. A /\ y e. ( F ` x ) ) } C_ A <-> A. y ( E. x ( x e. A /\ y e. ( F ` x ) ) -> y e. A ) )
34 32 33 bitri 
 |-  ( ran R C_ A <-> A. y ( E. x ( x e. A /\ y e. ( F ` x ) ) -> y e. A ) )
35 28 34 sylibr 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ran R C_ A )
36 35 19 sseqtrrd 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ran R C_ dom R )
37 36 adantl 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> ran R C_ dom R )
38 fvrn0 
 |-  ( F ` x ) e. ( ran F u. { (/) } )
39 elssuni 
 |-  ( ( F ` x ) e. ( ran F u. { (/) } ) -> ( F ` x ) C_ U. ( ran F u. { (/) } ) )
40 38 39 ax-mp 
 |-  ( F ` x ) C_ U. ( ran F u. { (/) } )
41 40 sseli 
 |-  ( y e. ( F ` x ) -> y e. U. ( ran F u. { (/) } ) )
42 41 anim2i 
 |-  ( ( x e. A /\ y e. ( F ` x ) ) -> ( x e. A /\ y e. U. ( ran F u. { (/) } ) ) )
43 42 ssopab2i 
 |-  { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } C_ { <. x , y >. | ( x e. A /\ y e. U. ( ran F u. { (/) } ) ) }
44 df-xp 
 |-  ( A X. U. ( ran F u. { (/) } ) ) = { <. x , y >. | ( x e. A /\ y e. U. ( ran F u. { (/) } ) ) }
45 43 2 44 3sstr4i 
 |-  R C_ ( A X. U. ( ran F u. { (/) } ) )
46 frn 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ran F C_ ( ~P A \ { (/) } ) )
47 46 adantl 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> ran F C_ ( ~P A \ { (/) } ) )
48 1 pwex 
 |-  ~P A e. _V
49 48 difexi 
 |-  ( ~P A \ { (/) } ) e. _V
50 49 ssex 
 |-  ( ran F C_ ( ~P A \ { (/) } ) -> ran F e. _V )
51 47 50 syl 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> ran F e. _V )
52 p0ex 
 |-  { (/) } e. _V
53 unexg 
 |-  ( ( ran F e. _V /\ { (/) } e. _V ) -> ( ran F u. { (/) } ) e. _V )
54 51 52 53 sylancl 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> ( ran F u. { (/) } ) e. _V )
55 54 uniexd 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> U. ( ran F u. { (/) } ) e. _V )
56 xpexg 
 |-  ( ( A e. _V /\ U. ( ran F u. { (/) } ) e. _V ) -> ( A X. U. ( ran F u. { (/) } ) ) e. _V )
57 1 55 56 sylancr 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> ( A X. U. ( ran F u. { (/) } ) ) e. _V )
58 ssexg 
 |-  ( ( R C_ ( A X. U. ( ran F u. { (/) } ) ) /\ ( A X. U. ( ran F u. { (/) } ) ) e. _V ) -> R e. _V )
59 45 57 58 sylancr 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> R e. _V )
60 n0 
 |-  ( dom r =/= (/) <-> E. x x e. dom r )
61 vex 
 |-  x e. _V
62 61 eldm 
 |-  ( x e. dom r <-> E. y x r y )
63 62 exbii 
 |-  ( E. x x e. dom r <-> E. x E. y x r y )
64 60 63 bitr2i 
 |-  ( E. x E. y x r y <-> dom r =/= (/) )
65 dmeq 
 |-  ( r = R -> dom r = dom R )
66 65 neeq1d 
 |-  ( r = R -> ( dom r =/= (/) <-> dom R =/= (/) ) )
67 64 66 bitrid 
 |-  ( r = R -> ( E. x E. y x r y <-> dom R =/= (/) ) )
68 rneq 
 |-  ( r = R -> ran r = ran R )
69 68 65 sseq12d 
 |-  ( r = R -> ( ran r C_ dom r <-> ran R C_ dom R ) )
70 67 69 anbi12d 
 |-  ( r = R -> ( ( E. x E. y x r y /\ ran r C_ dom r ) <-> ( dom R =/= (/) /\ ran R C_ dom R ) ) )
71 breq 
 |-  ( r = R -> ( ( h ` k ) r ( h ` suc k ) <-> ( h ` k ) R ( h ` suc k ) ) )
72 71 ralbidv 
 |-  ( r = R -> ( A. k e. _om ( h ` k ) r ( h ` suc k ) <-> A. k e. _om ( h ` k ) R ( h ` suc k ) ) )
73 72 exbidv 
 |-  ( r = R -> ( E. h A. k e. _om ( h ` k ) r ( h ` suc k ) <-> E. h A. k e. _om ( h ` k ) R ( h ` suc k ) ) )
74 70 73 imbi12d 
 |-  ( r = R -> ( ( ( E. x E. y x r y /\ ran r C_ dom r ) -> E. h A. k e. _om ( h ` k ) r ( h ` suc k ) ) <-> ( ( dom R =/= (/) /\ ran R C_ dom R ) -> E. h A. k e. _om ( h ` k ) R ( h ` suc k ) ) ) )
75 ax-dc 
 |-  ( ( E. x E. y x r y /\ ran r C_ dom r ) -> E. h A. k e. _om ( h ` k ) r ( h ` suc k ) )
76 74 75 vtoclg 
 |-  ( R e. _V -> ( ( dom R =/= (/) /\ ran R C_ dom R ) -> E. h A. k e. _om ( h ` k ) R ( h ` suc k ) ) )
77 59 76 syl 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> ( ( dom R =/= (/) /\ ran R C_ dom R ) -> E. h A. k e. _om ( h ` k ) R ( h ` suc k ) ) )
78 21 37 77 mp2and 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> E. h A. k e. _om ( h ` k ) R ( h ` suc k ) )
79 simpr 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> F : A --> ( ~P A \ { (/) } ) )
80 fveq2 
 |-  ( k = x -> ( h ` k ) = ( h ` x ) )
81 suceq 
 |-  ( k = x -> suc k = suc x )
82 81 fveq2d 
 |-  ( k = x -> ( h ` suc k ) = ( h ` suc x ) )
83 80 82 breq12d 
 |-  ( k = x -> ( ( h ` k ) R ( h ` suc k ) <-> ( h ` x ) R ( h ` suc x ) ) )
84 83 rspccv 
 |-  ( A. k e. _om ( h ` k ) R ( h ` suc k ) -> ( x e. _om -> ( h ` x ) R ( h ` suc x ) ) )
85 fvex 
 |-  ( h ` x ) e. _V
86 fvex 
 |-  ( h ` suc x ) e. _V
87 85 86 breldm 
 |-  ( ( h ` x ) R ( h ` suc x ) -> ( h ` x ) e. dom R )
88 84 87 syl6 
 |-  ( A. k e. _om ( h ` k ) R ( h ` suc k ) -> ( x e. _om -> ( h ` x ) e. dom R ) )
89 88 imp 
 |-  ( ( A. k e. _om ( h ` k ) R ( h ` suc k ) /\ x e. _om ) -> ( h ` x ) e. dom R )
90 89 adantll 
 |-  ( ( ( dom R = A /\ A. k e. _om ( h ` k ) R ( h ` suc k ) ) /\ x e. _om ) -> ( h ` x ) e. dom R )
91 eleq2 
 |-  ( dom R = A -> ( ( h ` x ) e. dom R <-> ( h ` x ) e. A ) )
92 91 ad2antrr 
 |-  ( ( ( dom R = A /\ A. k e. _om ( h ` k ) R ( h ` suc k ) ) /\ x e. _om ) -> ( ( h ` x ) e. dom R <-> ( h ` x ) e. A ) )
93 90 92 mpbid 
 |-  ( ( ( dom R = A /\ A. k e. _om ( h ` k ) R ( h ` suc k ) ) /\ x e. _om ) -> ( h ` x ) e. A )
94 93 3 fmptd 
 |-  ( ( dom R = A /\ A. k e. _om ( h ` k ) R ( h ` suc k ) ) -> G : _om --> A )
95 94 ex 
 |-  ( dom R = A -> ( A. k e. _om ( h ` k ) R ( h ` suc k ) -> G : _om --> A ) )
96 19 95 syl 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( A. k e. _om ( h ` k ) R ( h ` suc k ) -> G : _om --> A ) )
97 96 impcom 
 |-  ( ( A. k e. _om ( h ` k ) R ( h ` suc k ) /\ F : A --> ( ~P A \ { (/) } ) ) -> G : _om --> A )
98 fveq2 
 |-  ( x = k -> ( h ` x ) = ( h ` k ) )
99 fvex 
 |-  ( h ` k ) e. _V
100 98 3 99 fvmpt 
 |-  ( k e. _om -> ( G ` k ) = ( h ` k ) )
101 peano2 
 |-  ( k e. _om -> suc k e. _om )
102 fvex 
 |-  ( h ` suc k ) e. _V
103 fveq2 
 |-  ( x = suc k -> ( h ` x ) = ( h ` suc k ) )
104 103 3 fvmptg 
 |-  ( ( suc k e. _om /\ ( h ` suc k ) e. _V ) -> ( G ` suc k ) = ( h ` suc k ) )
105 101 102 104 sylancl 
 |-  ( k e. _om -> ( G ` suc k ) = ( h ` suc k ) )
106 100 105 breq12d 
 |-  ( k e. _om -> ( ( G ` k ) R ( G ` suc k ) <-> ( h ` k ) R ( h ` suc k ) ) )
107 fvex 
 |-  ( G ` k ) e. _V
108 fvex 
 |-  ( G ` suc k ) e. _V
109 eleq1 
 |-  ( x = ( G ` k ) -> ( x e. A <-> ( G ` k ) e. A ) )
110 fveq2 
 |-  ( x = ( G ` k ) -> ( F ` x ) = ( F ` ( G ` k ) ) )
111 110 eleq2d 
 |-  ( x = ( G ` k ) -> ( y e. ( F ` x ) <-> y e. ( F ` ( G ` k ) ) ) )
112 109 111 anbi12d 
 |-  ( x = ( G ` k ) -> ( ( x e. A /\ y e. ( F ` x ) ) <-> ( ( G ` k ) e. A /\ y e. ( F ` ( G ` k ) ) ) ) )
113 eleq1 
 |-  ( y = ( G ` suc k ) -> ( y e. ( F ` ( G ` k ) ) <-> ( G ` suc k ) e. ( F ` ( G ` k ) ) ) )
114 113 anbi2d 
 |-  ( y = ( G ` suc k ) -> ( ( ( G ` k ) e. A /\ y e. ( F ` ( G ` k ) ) ) <-> ( ( G ` k ) e. A /\ ( G ` suc k ) e. ( F ` ( G ` k ) ) ) ) )
115 107 108 112 114 2 brab 
 |-  ( ( G ` k ) R ( G ` suc k ) <-> ( ( G ` k ) e. A /\ ( G ` suc k ) e. ( F ` ( G ` k ) ) ) )
116 115 simprbi 
 |-  ( ( G ` k ) R ( G ` suc k ) -> ( G ` suc k ) e. ( F ` ( G ` k ) ) )
117 106 116 biimtrrdi 
 |-  ( k e. _om -> ( ( h ` k ) R ( h ` suc k ) -> ( G ` suc k ) e. ( F ` ( G ` k ) ) ) )
118 117 ralimia 
 |-  ( A. k e. _om ( h ` k ) R ( h ` suc k ) -> A. k e. _om ( G ` suc k ) e. ( F ` ( G ` k ) ) )
119 118 adantr 
 |-  ( ( A. k e. _om ( h ` k ) R ( h ` suc k ) /\ F : A --> ( ~P A \ { (/) } ) ) -> A. k e. _om ( G ` suc k ) e. ( F ` ( G ` k ) ) )
120 fvrn0 
 |-  ( h ` x ) e. ( ran h u. { (/) } )
121 120 rgenw 
 |-  A. x e. _om ( h ` x ) e. ( ran h u. { (/) } )
122 eqid 
 |-  ( x e. _om |-> ( h ` x ) ) = ( x e. _om |-> ( h ` x ) )
123 122 fmpt 
 |-  ( A. x e. _om ( h ` x ) e. ( ran h u. { (/) } ) <-> ( x e. _om |-> ( h ` x ) ) : _om --> ( ran h u. { (/) } ) )
124 121 123 mpbi 
 |-  ( x e. _om |-> ( h ` x ) ) : _om --> ( ran h u. { (/) } )
125 dcomex 
 |-  _om e. _V
126 vex 
 |-  h e. _V
127 126 rnex 
 |-  ran h e. _V
128 127 52 unex 
 |-  ( ran h u. { (/) } ) e. _V
129 fex2 
 |-  ( ( ( x e. _om |-> ( h ` x ) ) : _om --> ( ran h u. { (/) } ) /\ _om e. _V /\ ( ran h u. { (/) } ) e. _V ) -> ( x e. _om |-> ( h ` x ) ) e. _V )
130 124 125 128 129 mp3an 
 |-  ( x e. _om |-> ( h ` x ) ) e. _V
131 3 130 eqeltri 
 |-  G e. _V
132 feq1 
 |-  ( g = G -> ( g : _om --> A <-> G : _om --> A ) )
133 fveq1 
 |-  ( g = G -> ( g ` suc k ) = ( G ` suc k ) )
134 fveq1 
 |-  ( g = G -> ( g ` k ) = ( G ` k ) )
135 134 fveq2d 
 |-  ( g = G -> ( F ` ( g ` k ) ) = ( F ` ( G ` k ) ) )
136 133 135 eleq12d 
 |-  ( g = G -> ( ( g ` suc k ) e. ( F ` ( g ` k ) ) <-> ( G ` suc k ) e. ( F ` ( G ` k ) ) ) )
137 136 ralbidv 
 |-  ( g = G -> ( A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) <-> A. k e. _om ( G ` suc k ) e. ( F ` ( G ` k ) ) ) )
138 132 137 anbi12d 
 |-  ( g = G -> ( ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) <-> ( G : _om --> A /\ A. k e. _om ( G ` suc k ) e. ( F ` ( G ` k ) ) ) ) )
139 131 138 spcev 
 |-  ( ( G : _om --> A /\ A. k e. _om ( G ` suc k ) e. ( F ` ( G ` k ) ) ) -> E. g ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )
140 97 119 139 syl2anc 
 |-  ( ( A. k e. _om ( h ` k ) R ( h ` suc k ) /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )
141 140 ex 
 |-  ( A. k e. _om ( h ` k ) R ( h ` suc k ) -> ( F : A --> ( ~P A \ { (/) } ) -> E. g ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) ) )
142 141 exlimiv 
 |-  ( E. h A. k e. _om ( h ` k ) R ( h ` suc k ) -> ( F : A --> ( ~P A \ { (/) } ) -> E. g ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) ) )
143 78 79 142 sylc 
 |-  ( ( A =/= (/) /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )