Metamath Proof Explorer

Theorem axdc3lem4

Description: Lemma for axdc3 . We have constructed a "candidate set" S , which consists of all finite sequences s that satisfy our property of interest, namely s ( x + 1 ) e. F ( s ( x ) ) on its domain, but with the added constraint that s ( 0 ) = C . These sets are possible "initial segments" of theinfinite sequence satisfying these constraints, but we can leverage the standard ax-dc (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely ( hn ) : m --> A (for some integer m ). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that S is nonempty, and that G always maps to a nonempty subset of S , so that we can apply axdc2 . See axdc3lem2 for the rest of the proof. (Contributed by Mario Carneiro, 27-Jan-2013)

Ref Expression
Hypotheses axdc3lem4.1 
|- A e. _V
axdc3lem4.2 
|- S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
axdc3lem4.3 
|- G = ( x e. S |-> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } )
Assertion axdc3lem4 
|- ( ( C e. A /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc3lem4.1 
 |-  A e. _V
2 axdc3lem4.2 
 |-  S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
3 axdc3lem4.3 
 |-  G = ( x e. S |-> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } )
4 peano1 
 |-  (/) e. _om
5 eqid 
 |-  { <. (/) , C >. } = { <. (/) , C >. }
6 fsng 
 |-  ( ( (/) e. _om /\ C e. A ) -> ( { <. (/) , C >. } : { (/) } --> { C } <-> { <. (/) , C >. } = { <. (/) , C >. } ) )
7 4 6 mpan 
 |-  ( C e. A -> ( { <. (/) , C >. } : { (/) } --> { C } <-> { <. (/) , C >. } = { <. (/) , C >. } ) )
8 5 7 mpbiri 
 |-  ( C e. A -> { <. (/) , C >. } : { (/) } --> { C } )
9 snssi 
 |-  ( C e. A -> { C } C_ A )
10 8 9 fssd 
 |-  ( C e. A -> { <. (/) , C >. } : { (/) } --> A )
11 suc0 
 |-  suc (/) = { (/) }
12 11 feq2i 
 |-  ( { <. (/) , C >. } : suc (/) --> A <-> { <. (/) , C >. } : { (/) } --> A )
13 10 12 sylibr 
 |-  ( C e. A -> { <. (/) , C >. } : suc (/) --> A )
14 fvsng 
 |-  ( ( (/) e. _om /\ C e. A ) -> ( { <. (/) , C >. } ` (/) ) = C )
15 4 14 mpan 
 |-  ( C e. A -> ( { <. (/) , C >. } ` (/) ) = C )
16 ral0 
 |-  A. k e. (/) ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) )
17 16 a1i 
 |-  ( C e. A -> A. k e. (/) ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) )
18 13 15 17 3jca 
 |-  ( C e. A -> ( { <. (/) , C >. } : suc (/) --> A /\ ( { <. (/) , C >. } ` (/) ) = C /\ A. k e. (/) ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) )
19 suceq 
 |-  ( m = (/) -> suc m = suc (/) )
20 19 feq2d 
 |-  ( m = (/) -> ( { <. (/) , C >. } : suc m --> A <-> { <. (/) , C >. } : suc (/) --> A ) )
21 raleq 
 |-  ( m = (/) -> ( A. k e. m ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) <-> A. k e. (/) ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) )
22 20 21 3anbi13d 
 |-  ( m = (/) -> ( ( { <. (/) , C >. } : suc m --> A /\ ( { <. (/) , C >. } ` (/) ) = C /\ A. k e. m ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) <-> ( { <. (/) , C >. } : suc (/) --> A /\ ( { <. (/) , C >. } ` (/) ) = C /\ A. k e. (/) ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) ) )
23 22 rspcev 
 |-  ( ( (/) e. _om /\ ( { <. (/) , C >. } : suc (/) --> A /\ ( { <. (/) , C >. } ` (/) ) = C /\ A. k e. (/) ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) ) -> E. m e. _om ( { <. (/) , C >. } : suc m --> A /\ ( { <. (/) , C >. } ` (/) ) = C /\ A. k e. m ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) )
24 4 18 23 sylancr 
 |-  ( C e. A -> E. m e. _om ( { <. (/) , C >. } : suc m --> A /\ ( { <. (/) , C >. } ` (/) ) = C /\ A. k e. m ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) )
25 snex 
 |-  { <. (/) , C >. } e. _V
26 1 2 25 axdc3lem3 
 |-  ( { <. (/) , C >. } e. S <-> E. m e. _om ( { <. (/) , C >. } : suc m --> A /\ ( { <. (/) , C >. } ` (/) ) = C /\ A. k e. m ( { <. (/) , C >. } ` suc k ) e. ( F ` ( { <. (/) , C >. } ` k ) ) ) )
27 24 26 sylibr 
 |-  ( C e. A -> { <. (/) , C >. } e. S )
28 27 ne0d 
 |-  ( C e. A -> S =/= (/) )
29 1 2 axdc3lem 
 |-  S e. _V
30 ssrab2 
 |-  { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } C_ S
31 29 30 elpwi2 
 |-  { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } e. ~P S
32 31 a1i 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. S ) -> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } e. ~P S )
33 vex 
 |-  x e. _V
34 1 2 33 axdc3lem3 
 |-  ( x e. S <-> E. m e. _om ( x : suc m --> A /\ ( x ` (/) ) = C /\ A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) ) )
35 simp2 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> x : suc m --> A )
36 vex 
 |-  m e. _V
37 36 sucid 
 |-  m e. suc m
38 ffvelrn 
 |-  ( ( x : suc m --> A /\ m e. suc m ) -> ( x ` m ) e. A )
39 37 38 mpan2 
 |-  ( x : suc m --> A -> ( x ` m ) e. A )
40 ffvelrn 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ ( x ` m ) e. A ) -> ( F ` ( x ` m ) ) e. ( ~P A \ { (/) } ) )
41 39 40 sylan2 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> ( F ` ( x ` m ) ) e. ( ~P A \ { (/) } ) )
42 eldifn 
 |-  ( ( F ` ( x ` m ) ) e. ( ~P A \ { (/) } ) -> -. ( F ` ( x ` m ) ) e. { (/) } )
43 fvex 
 |-  ( F ` ( x ` m ) ) e. _V
44 43 elsn 
 |-  ( ( F ` ( x ` m ) ) e. { (/) } <-> ( F ` ( x ` m ) ) = (/) )
45 44 necon3bbii 
 |-  ( -. ( F ` ( x ` m ) ) e. { (/) } <-> ( F ` ( x ` m ) ) =/= (/) )
46 n0 
 |-  ( ( F ` ( x ` m ) ) =/= (/) <-> E. z z e. ( F ` ( x ` m ) ) )
47 45 46 bitri 
 |-  ( -. ( F ` ( x ` m ) ) e. { (/) } <-> E. z z e. ( F ` ( x ` m ) ) )
48 42 47 sylib 
 |-  ( ( F ` ( x ` m ) ) e. ( ~P A \ { (/) } ) -> E. z z e. ( F ` ( x ` m ) ) )
49 41 48 syl 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> E. z z e. ( F ` ( x ` m ) ) )
50 simp32 
 |-  ( ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) -> x : suc m --> A )
51 eldifi 
 |-  ( ( F ` ( x ` m ) ) e. ( ~P A \ { (/) } ) -> ( F ` ( x ` m ) ) e. ~P A )
52 elelpwi 
 |-  ( ( z e. ( F ` ( x ` m ) ) /\ ( F ` ( x ` m ) ) e. ~P A ) -> z e. A )
53 52 expcom 
 |-  ( ( F ` ( x ` m ) ) e. ~P A -> ( z e. ( F ` ( x ` m ) ) -> z e. A ) )
54 41 51 53 3syl 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> z e. A ) )
55 peano2 
 |-  ( m e. _om -> suc m e. _om )
56 55 3ad2ant3 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> suc m e. _om )
57 56 3ad2ant1 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> suc m e. _om )
58 simplr 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> x : suc m --> A )
59 33 dmex 
 |-  dom x e. _V
60 vex 
 |-  z e. _V
61 eqid 
 |-  { <. dom x , z >. } = { <. dom x , z >. }
62 fsng 
 |-  ( ( dom x e. _V /\ z e. _V ) -> ( { <. dom x , z >. } : { dom x } --> { z } <-> { <. dom x , z >. } = { <. dom x , z >. } ) )
63 61 62 mpbiri 
 |-  ( ( dom x e. _V /\ z e. _V ) -> { <. dom x , z >. } : { dom x } --> { z } )
64 59 60 63 mp2an 
 |-  { <. dom x , z >. } : { dom x } --> { z }
65 simpr 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> z e. A )
66 65 snssd 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> { z } C_ A )
67 fss 
 |-  ( ( { <. dom x , z >. } : { dom x } --> { z } /\ { z } C_ A ) -> { <. dom x , z >. } : { dom x } --> A )
68 64 66 67 sylancr 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> { <. dom x , z >. } : { dom x } --> A )
69 fdm 
 |-  ( x : suc m --> A -> dom x = suc m )
70 55 adantr 
 |-  ( ( m e. _om /\ dom x = suc m ) -> suc m e. _om )
71 eleq1 
 |-  ( dom x = suc m -> ( dom x e. _om <-> suc m e. _om ) )
72 71 adantl 
 |-  ( ( m e. _om /\ dom x = suc m ) -> ( dom x e. _om <-> suc m e. _om ) )
73 70 72 mpbird 
 |-  ( ( m e. _om /\ dom x = suc m ) -> dom x e. _om )
74 nnord 
 |-  ( dom x e. _om -> Ord dom x )
75 ordirr 
 |-  ( Ord dom x -> -. dom x e. dom x )
76 73 74 75 3syl 
 |-  ( ( m e. _om /\ dom x = suc m ) -> -. dom x e. dom x )
77 eleq2 
 |-  ( dom x = suc m -> ( dom x e. dom x <-> dom x e. suc m ) )
78 77 adantl 
 |-  ( ( m e. _om /\ dom x = suc m ) -> ( dom x e. dom x <-> dom x e. suc m ) )
79 76 78 mtbid 
 |-  ( ( m e. _om /\ dom x = suc m ) -> -. dom x e. suc m )
80 disjsn 
 |-  ( ( suc m i^i { dom x } ) = (/) <-> -. dom x e. suc m )
81 79 80 sylibr 
 |-  ( ( m e. _om /\ dom x = suc m ) -> ( suc m i^i { dom x } ) = (/) )
82 69 81 sylan2 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( suc m i^i { dom x } ) = (/) )
83 82 adantr 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> ( suc m i^i { dom x } ) = (/) )
84 58 68 83 fun2d 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> ( x u. { <. dom x , z >. } ) : ( suc m u. { dom x } ) --> A )
85 sneq 
 |-  ( dom x = suc m -> { dom x } = { suc m } )
86 85 uneq2d 
 |-  ( dom x = suc m -> ( suc m u. { dom x } ) = ( suc m u. { suc m } ) )
87 df-suc 
 |-  suc suc m = ( suc m u. { suc m } )
88 86 87 eqtr4di 
 |-  ( dom x = suc m -> ( suc m u. { dom x } ) = suc suc m )
89 69 88 syl 
 |-  ( x : suc m --> A -> ( suc m u. { dom x } ) = suc suc m )
90 89 ad2antlr 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> ( suc m u. { dom x } ) = suc suc m )
91 90 feq2d 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> ( ( x u. { <. dom x , z >. } ) : ( suc m u. { dom x } ) --> A <-> ( x u. { <. dom x , z >. } ) : suc suc m --> A ) )
92 84 91 mpbid 
 |-  ( ( ( m e. _om /\ x : suc m --> A ) /\ z e. A ) -> ( x u. { <. dom x , z >. } ) : suc suc m --> A )
93 92 ex 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( z e. A -> ( x u. { <. dom x , z >. } ) : suc suc m --> A ) )
94 93 adantrd 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( ( z e. A /\ ( x ` (/) ) = C ) -> ( x u. { <. dom x , z >. } ) : suc suc m --> A ) )
95 94 a1d 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( z e. A /\ ( x ` (/) ) = C ) -> ( x u. { <. dom x , z >. } ) : suc suc m --> A ) ) )
96 95 ancoms 
 |-  ( ( x : suc m --> A /\ m e. _om ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( z e. A /\ ( x ` (/) ) = C ) -> ( x u. { <. dom x , z >. } ) : suc suc m --> A ) ) )
97 96 3adant1 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( z e. A /\ ( x ` (/) ) = C ) -> ( x u. { <. dom x , z >. } ) : suc suc m --> A ) ) )
98 97 3imp 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> ( x u. { <. dom x , z >. } ) : suc suc m --> A )
99 ffun 
 |-  ( x : suc m --> A -> Fun x )
100 99 adantl 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> Fun x )
101 59 60 funsn 
 |-  Fun { <. dom x , z >. }
102 100 101 jctir 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( Fun x /\ Fun { <. dom x , z >. } ) )
103 60 dmsnop 
 |-  dom { <. dom x , z >. } = { dom x }
104 103 ineq2i 
 |-  ( dom x i^i dom { <. dom x , z >. } ) = ( dom x i^i { dom x } )
105 disjsn 
 |-  ( ( dom x i^i { dom x } ) = (/) <-> -. dom x e. dom x )
106 76 105 sylibr 
 |-  ( ( m e. _om /\ dom x = suc m ) -> ( dom x i^i { dom x } ) = (/) )
107 104 106 syl5eq 
 |-  ( ( m e. _om /\ dom x = suc m ) -> ( dom x i^i dom { <. dom x , z >. } ) = (/) )
108 69 107 sylan2 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( dom x i^i dom { <. dom x , z >. } ) = (/) )
109 funun 
 |-  ( ( ( Fun x /\ Fun { <. dom x , z >. } ) /\ ( dom x i^i dom { <. dom x , z >. } ) = (/) ) -> Fun ( x u. { <. dom x , z >. } ) )
110 102 108 109 syl2anc 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> Fun ( x u. { <. dom x , z >. } ) )
111 ssun1 
 |-  x C_ ( x u. { <. dom x , z >. } )
112 111 a1i 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> x C_ ( x u. { <. dom x , z >. } ) )
113 nnord 
 |-  ( m e. _om -> Ord m )
114 0elsuc 
 |-  ( Ord m -> (/) e. suc m )
115 113 114 syl 
 |-  ( m e. _om -> (/) e. suc m )
116 115 adantr 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> (/) e. suc m )
117 69 eleq2d 
 |-  ( x : suc m --> A -> ( (/) e. dom x <-> (/) e. suc m ) )
118 117 adantl 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( (/) e. dom x <-> (/) e. suc m ) )
119 116 118 mpbird 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> (/) e. dom x )
120 funssfv 
 |-  ( ( Fun ( x u. { <. dom x , z >. } ) /\ x C_ ( x u. { <. dom x , z >. } ) /\ (/) e. dom x ) -> ( ( x u. { <. dom x , z >. } ) ` (/) ) = ( x ` (/) ) )
121 110 112 119 120 syl3anc 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` (/) ) = ( x ` (/) ) )
122 121 eqeq1d 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( ( ( x u. { <. dom x , z >. } ) ` (/) ) = C <-> ( x ` (/) ) = C ) )
123 122 ancoms 
 |-  ( ( x : suc m --> A /\ m e. _om ) -> ( ( ( x u. { <. dom x , z >. } ) ` (/) ) = C <-> ( x ` (/) ) = C ) )
124 123 3adant1 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( ( ( x u. { <. dom x , z >. } ) ` (/) ) = C <-> ( x ` (/) ) = C ) )
125 124 biimpar 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ ( x ` (/) ) = C ) -> ( ( x u. { <. dom x , z >. } ) ` (/) ) = C )
126 125 adantrl 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> ( ( x u. { <. dom x , z >. } ) ` (/) ) = C )
127 126 3adant2 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> ( ( x u. { <. dom x , z >. } ) ` (/) ) = C )
128 nfra1 
 |-  F/ k A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) )
129 nfv 
 |-  F/ k x : suc m --> A
130 nfv 
 |-  F/ k m e. _om
131 128 129 130 nf3an 
 |-  F/ k ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om )
132 nfv 
 |-  F/ k z e. ( F ` ( x ` m ) )
133 nfv 
 |-  F/ k ( z e. A /\ ( x ` (/) ) = C )
134 131 132 133 nf3an 
 |-  F/ k ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) )
135 simplr 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> k e. suc m )
136 elsuci 
 |-  ( k e. suc m -> ( k e. m \/ k = m ) )
137 rsp 
 |-  ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) -> ( k e. m -> ( x ` suc k ) e. ( F ` ( x ` k ) ) ) )
138 137 impcom 
 |-  ( ( k e. m /\ A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) ) -> ( x ` suc k ) e. ( F ` ( x ` k ) ) )
139 138 ad2ant2lr 
 |-  ( ( ( m e. _om /\ k e. m ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) ) -> ( x ` suc k ) e. ( F ` ( x ` k ) ) )
140 139 3adant3 
 |-  ( ( ( m e. _om /\ k e. m ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( x ` suc k ) e. ( F ` ( x ` k ) ) )
141 110 adantlr 
 |-  ( ( ( m e. _om /\ k e. m ) /\ x : suc m --> A ) -> Fun ( x u. { <. dom x , z >. } ) )
142 111 a1i 
 |-  ( ( ( m e. _om /\ k e. m ) /\ x : suc m --> A ) -> x C_ ( x u. { <. dom x , z >. } ) )
143 ordsucelsuc 
 |-  ( Ord m -> ( k e. m <-> suc k e. suc m ) )
144 113 143 syl 
 |-  ( m e. _om -> ( k e. m <-> suc k e. suc m ) )
145 144 biimpa 
 |-  ( ( m e. _om /\ k e. m ) -> suc k e. suc m )
146 eleq2 
 |-  ( dom x = suc m -> ( suc k e. dom x <-> suc k e. suc m ) )
147 146 biimparc 
 |-  ( ( suc k e. suc m /\ dom x = suc m ) -> suc k e. dom x )
148 145 69 147 syl2an 
 |-  ( ( ( m e. _om /\ k e. m ) /\ x : suc m --> A ) -> suc k e. dom x )
149 funssfv 
 |-  ( ( Fun ( x u. { <. dom x , z >. } ) /\ x C_ ( x u. { <. dom x , z >. } ) /\ suc k e. dom x ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = ( x ` suc k ) )
150 141 142 148 149 syl3anc 
 |-  ( ( ( m e. _om /\ k e. m ) /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = ( x ` suc k ) )
151 150 3adant2 
 |-  ( ( ( m e. _om /\ k e. m ) /\ k e. suc m /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = ( x ` suc k ) )
152 110 3adant2 
 |-  ( ( m e. _om /\ k e. suc m /\ x : suc m --> A ) -> Fun ( x u. { <. dom x , z >. } ) )
153 111 a1i 
 |-  ( ( m e. _om /\ k e. suc m /\ x : suc m --> A ) -> x C_ ( x u. { <. dom x , z >. } ) )
154 eleq2 
 |-  ( dom x = suc m -> ( k e. dom x <-> k e. suc m ) )
155 154 biimparc 
 |-  ( ( k e. suc m /\ dom x = suc m ) -> k e. dom x )
156 69 155 sylan2 
 |-  ( ( k e. suc m /\ x : suc m --> A ) -> k e. dom x )
157 156 3adant1 
 |-  ( ( m e. _om /\ k e. suc m /\ x : suc m --> A ) -> k e. dom x )
158 funssfv 
 |-  ( ( Fun ( x u. { <. dom x , z >. } ) /\ x C_ ( x u. { <. dom x , z >. } ) /\ k e. dom x ) -> ( ( x u. { <. dom x , z >. } ) ` k ) = ( x ` k ) )
159 152 153 157 158 syl3anc 
 |-  ( ( m e. _om /\ k e. suc m /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` k ) = ( x ` k ) )
160 159 3adant1r 
 |-  ( ( ( m e. _om /\ k e. m ) /\ k e. suc m /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` k ) = ( x ` k ) )
161 160 fveq2d 
 |-  ( ( ( m e. _om /\ k e. m ) /\ k e. suc m /\ x : suc m --> A ) -> ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) = ( F ` ( x ` k ) ) )
162 151 161 eleq12d 
 |-  ( ( ( m e. _om /\ k e. m ) /\ k e. suc m /\ x : suc m --> A ) -> ( ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) <-> ( x ` suc k ) e. ( F ` ( x ` k ) ) ) )
163 162 3adant2l 
 |-  ( ( ( m e. _om /\ k e. m ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) <-> ( x ` suc k ) e. ( F ` ( x ` k ) ) ) )
164 140 163 mpbird 
 |-  ( ( ( m e. _om /\ k e. m ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) )
165 164 a1d 
 |-  ( ( ( m e. _om /\ k e. m ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
166 165 3expib 
 |-  ( ( m e. _om /\ k e. m ) -> ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) )
167 166 expcom 
 |-  ( k e. m -> ( m e. _om -> ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) ) )
168 110 3adant1 
 |-  ( ( k = m /\ m e. _om /\ x : suc m --> A ) -> Fun ( x u. { <. dom x , z >. } ) )
169 ssun2 
 |-  { <. dom x , z >. } C_ ( x u. { <. dom x , z >. } )
170 169 a1i 
 |-  ( ( k = m /\ m e. _om /\ x : suc m --> A ) -> { <. dom x , z >. } C_ ( x u. { <. dom x , z >. } ) )
171 suceq 
 |-  ( k = m -> suc k = suc m )
172 171 eqeq2d 
 |-  ( k = m -> ( dom x = suc k <-> dom x = suc m ) )
173 172 biimpar 
 |-  ( ( k = m /\ dom x = suc m ) -> dom x = suc k )
174 59 snid 
 |-  dom x e. { dom x }
175 174 103 eleqtrri 
 |-  dom x e. dom { <. dom x , z >. }
176 173 175 eqeltrrdi 
 |-  ( ( k = m /\ dom x = suc m ) -> suc k e. dom { <. dom x , z >. } )
177 69 176 sylan2 
 |-  ( ( k = m /\ x : suc m --> A ) -> suc k e. dom { <. dom x , z >. } )
178 177 3adant2 
 |-  ( ( k = m /\ m e. _om /\ x : suc m --> A ) -> suc k e. dom { <. dom x , z >. } )
179 funssfv 
 |-  ( ( Fun ( x u. { <. dom x , z >. } ) /\ { <. dom x , z >. } C_ ( x u. { <. dom x , z >. } ) /\ suc k e. dom { <. dom x , z >. } ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = ( { <. dom x , z >. } ` suc k ) )
180 168 170 178 179 syl3anc 
 |-  ( ( k = m /\ m e. _om /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = ( { <. dom x , z >. } ` suc k ) )
181 173 3adant2 
 |-  ( ( k = m /\ m e. _om /\ dom x = suc m ) -> dom x = suc k )
182 59 60 fvsn 
 |-  ( { <. dom x , z >. } ` dom x ) = z
183 fveq2 
 |-  ( dom x = suc k -> ( { <. dom x , z >. } ` dom x ) = ( { <. dom x , z >. } ` suc k ) )
184 182 183 syl5reqr 
 |-  ( dom x = suc k -> ( { <. dom x , z >. } ` suc k ) = z )
185 181 184 syl 
 |-  ( ( k = m /\ m e. _om /\ dom x = suc m ) -> ( { <. dom x , z >. } ` suc k ) = z )
186 69 185 syl3an3 
 |-  ( ( k = m /\ m e. _om /\ x : suc m --> A ) -> ( { <. dom x , z >. } ` suc k ) = z )
187 180 186 eqtrd 
 |-  ( ( k = m /\ m e. _om /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = z )
188 187 3expa 
 |-  ( ( ( k = m /\ m e. _om ) /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = z )
189 188 3adant2 
 |-  ( ( ( k = m /\ m e. _om ) /\ k e. suc m /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) = z )
190 159 3adant1l 
 |-  ( ( ( k = m /\ m e. _om ) /\ k e. suc m /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` k ) = ( x ` k ) )
191 fveq2 
 |-  ( k = m -> ( x ` k ) = ( x ` m ) )
192 191 adantr 
 |-  ( ( k = m /\ m e. _om ) -> ( x ` k ) = ( x ` m ) )
193 192 3ad2ant1 
 |-  ( ( ( k = m /\ m e. _om ) /\ k e. suc m /\ x : suc m --> A ) -> ( x ` k ) = ( x ` m ) )
194 190 193 eqtrd 
 |-  ( ( ( k = m /\ m e. _om ) /\ k e. suc m /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) ` k ) = ( x ` m ) )
195 194 fveq2d 
 |-  ( ( ( k = m /\ m e. _om ) /\ k e. suc m /\ x : suc m --> A ) -> ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) = ( F ` ( x ` m ) ) )
196 189 195 eleq12d 
 |-  ( ( ( k = m /\ m e. _om ) /\ k e. suc m /\ x : suc m --> A ) -> ( ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) <-> z e. ( F ` ( x ` m ) ) ) )
197 196 3adant2l 
 |-  ( ( ( k = m /\ m e. _om ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) <-> z e. ( F ` ( x ` m ) ) ) )
198 197 biimprd 
 |-  ( ( ( k = m /\ m e. _om ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
199 198 3expib 
 |-  ( ( k = m /\ m e. _om ) -> ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) )
200 199 ex 
 |-  ( k = m -> ( m e. _om -> ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) ) )
201 167 200 jaoi 
 |-  ( ( k e. m \/ k = m ) -> ( m e. _om -> ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) ) )
202 136 201 syl 
 |-  ( k e. suc m -> ( m e. _om -> ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) ) )
203 202 com3r 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( k e. suc m -> ( m e. _om -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) ) )
204 135 203 mpd 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) /\ x : suc m --> A ) -> ( m e. _om -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) )
205 204 ex 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ k e. suc m ) -> ( x : suc m --> A -> ( m e. _om -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) ) )
206 205 expcom 
 |-  ( k e. suc m -> ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) -> ( x : suc m --> A -> ( m e. _om -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) ) ) )
207 206 3impd 
 |-  ( k e. suc m -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) )
208 207 impd 
 |-  ( k e. suc m -> ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) ) -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
209 208 com12 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) ) -> ( k e. suc m -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
210 209 3adant3 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> ( k e. suc m -> ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
211 134 210 ralrimi 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> A. k e. suc m ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) )
212 suceq 
 |-  ( p = suc m -> suc p = suc suc m )
213 212 feq2d 
 |-  ( p = suc m -> ( ( x u. { <. dom x , z >. } ) : suc p --> A <-> ( x u. { <. dom x , z >. } ) : suc suc m --> A ) )
214 raleq 
 |-  ( p = suc m -> ( A. k e. p ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) <-> A. k e. suc m ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
215 213 214 3anbi13d 
 |-  ( p = suc m -> ( ( ( x u. { <. dom x , z >. } ) : suc p --> A /\ ( ( x u. { <. dom x , z >. } ) ` (/) ) = C /\ A. k e. p ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) <-> ( ( x u. { <. dom x , z >. } ) : suc suc m --> A /\ ( ( x u. { <. dom x , z >. } ) ` (/) ) = C /\ A. k e. suc m ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) )
216 215 rspcev 
 |-  ( ( suc m e. _om /\ ( ( x u. { <. dom x , z >. } ) : suc suc m --> A /\ ( ( x u. { <. dom x , z >. } ) ` (/) ) = C /\ A. k e. suc m ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) ) -> E. p e. _om ( ( x u. { <. dom x , z >. } ) : suc p --> A /\ ( ( x u. { <. dom x , z >. } ) ` (/) ) = C /\ A. k e. p ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
217 57 98 127 211 216 syl13anc 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> E. p e. _om ( ( x u. { <. dom x , z >. } ) : suc p --> A /\ ( ( x u. { <. dom x , z >. } ) ` (/) ) = C /\ A. k e. p ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
218 snex 
 |-  { <. dom x , z >. } e. _V
219 33 218 unex 
 |-  ( x u. { <. dom x , z >. } ) e. _V
220 1 2 219 axdc3lem3 
 |-  ( ( x u. { <. dom x , z >. } ) e. S <-> E. p e. _om ( ( x u. { <. dom x , z >. } ) : suc p --> A /\ ( ( x u. { <. dom x , z >. } ) ` (/) ) = C /\ A. k e. p ( ( x u. { <. dom x , z >. } ) ` suc k ) e. ( F ` ( ( x u. { <. dom x , z >. } ) ` k ) ) ) )
221 217 220 sylibr 
 |-  ( ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) /\ z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) ) -> ( x u. { <. dom x , z >. } ) e. S )
222 221 3coml 
 |-  ( ( z e. ( F ` ( x ` m ) ) /\ ( z e. A /\ ( x ` (/) ) = C ) /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) -> ( x u. { <. dom x , z >. } ) e. S )
223 222 3exp 
 |-  ( z e. ( F ` ( x ` m ) ) -> ( ( z e. A /\ ( x ` (/) ) = C ) -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( x u. { <. dom x , z >. } ) e. S ) ) )
224 223 expd 
 |-  ( z e. ( F ` ( x ` m ) ) -> ( z e. A -> ( ( x ` (/) ) = C -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( x u. { <. dom x , z >. } ) e. S ) ) ) )
225 54 224 sylcom 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x ` (/) ) = C -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( x u. { <. dom x , z >. } ) e. S ) ) ) )
226 225 3impd 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> ( ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) -> ( x u. { <. dom x , z >. } ) e. S ) )
227 226 ex 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( x : suc m --> A -> ( ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) -> ( x u. { <. dom x , z >. } ) e. S ) ) )
228 227 com23 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) -> ( x : suc m --> A -> ( x u. { <. dom x , z >. } ) e. S ) ) )
229 50 228 mpdi 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) -> ( x u. { <. dom x , z >. } ) e. S ) )
230 229 imp 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) ) -> ( x u. { <. dom x , z >. } ) e. S )
231 resundir 
 |-  ( ( x u. { <. dom x , z >. } ) |` dom x ) = ( ( x |` dom x ) u. ( { <. dom x , z >. } |` dom x ) )
232 frel 
 |-  ( x : suc m --> A -> Rel x )
233 resdm 
 |-  ( Rel x -> ( x |` dom x ) = x )
234 232 233 syl 
 |-  ( x : suc m --> A -> ( x |` dom x ) = x )
235 234 adantl 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( x |` dom x ) = x )
236 69 73 sylan2 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> dom x e. _om )
237 74 75 syl 
 |-  ( dom x e. _om -> -. dom x e. dom x )
238 incom 
 |-  ( { dom x } i^i dom x ) = ( dom x i^i { dom x } )
239 238 eqeq1i 
 |-  ( ( { dom x } i^i dom x ) = (/) <-> ( dom x i^i { dom x } ) = (/) )
240 59 60 fnsn 
 |-  { <. dom x , z >. } Fn { dom x }
241 fnresdisj 
 |-  ( { <. dom x , z >. } Fn { dom x } -> ( ( { dom x } i^i dom x ) = (/) <-> ( { <. dom x , z >. } |` dom x ) = (/) ) )
242 240 241 ax-mp 
 |-  ( ( { dom x } i^i dom x ) = (/) <-> ( { <. dom x , z >. } |` dom x ) = (/) )
243 239 242 105 3bitr3ri 
 |-  ( -. dom x e. dom x <-> ( { <. dom x , z >. } |` dom x ) = (/) )
244 237 243 sylib 
 |-  ( dom x e. _om -> ( { <. dom x , z >. } |` dom x ) = (/) )
245 236 244 syl 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( { <. dom x , z >. } |` dom x ) = (/) )
246 235 245 uneq12d 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( ( x |` dom x ) u. ( { <. dom x , z >. } |` dom x ) ) = ( x u. (/) ) )
247 un0 
 |-  ( x u. (/) ) = x
248 246 247 eqtrdi 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( ( x |` dom x ) u. ( { <. dom x , z >. } |` dom x ) ) = x )
249 231 248 syl5eq 
 |-  ( ( m e. _om /\ x : suc m --> A ) -> ( ( x u. { <. dom x , z >. } ) |` dom x ) = x )
250 249 ancoms 
 |-  ( ( x : suc m --> A /\ m e. _om ) -> ( ( x u. { <. dom x , z >. } ) |` dom x ) = x )
251 250 3adant1 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( ( x u. { <. dom x , z >. } ) |` dom x ) = x )
252 251 3ad2ant3 
 |-  ( ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) -> ( ( x u. { <. dom x , z >. } ) |` dom x ) = x )
253 252 adantl 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) ) -> ( ( x u. { <. dom x , z >. } ) |` dom x ) = x )
254 103 uneq2i 
 |-  ( dom x u. dom { <. dom x , z >. } ) = ( dom x u. { dom x } )
255 dmun 
 |-  dom ( x u. { <. dom x , z >. } ) = ( dom x u. dom { <. dom x , z >. } )
256 df-suc 
 |-  suc dom x = ( dom x u. { dom x } )
257 254 255 256 3eqtr4i 
 |-  dom ( x u. { <. dom x , z >. } ) = suc dom x
258 253 257 jctil 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) ) -> ( dom ( x u. { <. dom x , z >. } ) = suc dom x /\ ( ( x u. { <. dom x , z >. } ) |` dom x ) = x ) )
259 dmeq 
 |-  ( y = ( x u. { <. dom x , z >. } ) -> dom y = dom ( x u. { <. dom x , z >. } ) )
260 259 eqeq1d 
 |-  ( y = ( x u. { <. dom x , z >. } ) -> ( dom y = suc dom x <-> dom ( x u. { <. dom x , z >. } ) = suc dom x ) )
261 reseq1 
 |-  ( y = ( x u. { <. dom x , z >. } ) -> ( y |` dom x ) = ( ( x u. { <. dom x , z >. } ) |` dom x ) )
262 261 eqeq1d 
 |-  ( y = ( x u. { <. dom x , z >. } ) -> ( ( y |` dom x ) = x <-> ( ( x u. { <. dom x , z >. } ) |` dom x ) = x ) )
263 260 262 anbi12d 
 |-  ( y = ( x u. { <. dom x , z >. } ) -> ( ( dom y = suc dom x /\ ( y |` dom x ) = x ) <-> ( dom ( x u. { <. dom x , z >. } ) = suc dom x /\ ( ( x u. { <. dom x , z >. } ) |` dom x ) = x ) ) )
264 263 rspcev 
 |-  ( ( ( x u. { <. dom x , z >. } ) e. S /\ ( dom ( x u. { <. dom x , z >. } ) = suc dom x /\ ( ( x u. { <. dom x , z >. } ) |` dom x ) = x ) ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) )
265 230 258 264 syl2anc 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ ( z e. ( F ` ( x ` m ) ) /\ ( x ` (/) ) = C /\ ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) ) ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) )
266 265 3exp2 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( z e. ( F ` ( x ` m ) ) -> ( ( x ` (/) ) = C -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) ) )
267 266 exlimdv 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> ( E. z z e. ( F ` ( x ` m ) ) -> ( ( x ` (/) ) = C -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) ) )
268 267 adantr 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> ( E. z z e. ( F ` ( x ` m ) ) -> ( ( x ` (/) ) = C -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) ) )
269 49 268 mpd 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> ( ( x ` (/) ) = C -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) )
270 269 com3r 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( ( F : A --> ( ~P A \ { (/) } ) /\ x : suc m --> A ) -> ( ( x ` (/) ) = C -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) )
271 35 270 mpan2d 
 |-  ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( F : A --> ( ~P A \ { (/) } ) -> ( ( x ` (/) ) = C -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) )
272 271 com3r 
 |-  ( ( x ` (/) ) = C -> ( ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) /\ x : suc m --> A /\ m e. _om ) -> ( F : A --> ( ~P A \ { (/) } ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) )
273 272 3expd 
 |-  ( ( x ` (/) ) = C -> ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) -> ( x : suc m --> A -> ( m e. _om -> ( F : A --> ( ~P A \ { (/) } ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) ) ) )
274 273 com3r 
 |-  ( x : suc m --> A -> ( ( x ` (/) ) = C -> ( A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) -> ( m e. _om -> ( F : A --> ( ~P A \ { (/) } ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) ) ) )
275 274 3imp 
 |-  ( ( x : suc m --> A /\ ( x ` (/) ) = C /\ A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) ) -> ( m e. _om -> ( F : A --> ( ~P A \ { (/) } ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) )
276 275 com12 
 |-  ( m e. _om -> ( ( x : suc m --> A /\ ( x ` (/) ) = C /\ A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) ) -> ( F : A --> ( ~P A \ { (/) } ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) ) )
277 276 rexlimiv 
 |-  ( E. m e. _om ( x : suc m --> A /\ ( x ` (/) ) = C /\ A. k e. m ( x ` suc k ) e. ( F ` ( x ` k ) ) ) -> ( F : A --> ( ~P A \ { (/) } ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) )
278 34 277 sylbi 
 |-  ( x e. S -> ( F : A --> ( ~P A \ { (/) } ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) ) )
279 278 impcom 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. S ) -> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) )
280 rabn0 
 |-  ( { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } =/= (/) <-> E. y e. S ( dom y = suc dom x /\ ( y |` dom x ) = x ) )
281 279 280 sylibr 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. S ) -> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } =/= (/) )
282 29 rabex 
 |-  { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } e. _V
283 282 elsn 
 |-  ( { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } e. { (/) } <-> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } = (/) )
284 283 necon3bbii 
 |-  ( -. { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } e. { (/) } <-> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } =/= (/) )
285 281 284 sylibr 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. S ) -> -. { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } e. { (/) } )
286 32 285 eldifd 
 |-  ( ( F : A --> ( ~P A \ { (/) } ) /\ x e. S ) -> { y e. S | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } e. ( ~P S \ { (/) } ) )
287 286 3 fmptd 
 |-  ( F : A --> ( ~P A \ { (/) } ) -> G : S --> ( ~P S \ { (/) } ) )
288 29 axdc2 
 |-  ( ( S =/= (/) /\ G : S --> ( ~P S \ { (/) } ) ) -> E. h ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) )
289 28 287 288 syl2an 
 |-  ( ( C e. A /\ F : A --> ( ~P A \ { (/) } ) ) -> E. h ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) )
290 1 2 3 axdc3lem2 
 |-  ( E. h ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )
291 289 290 syl 
 |-  ( ( C e. A /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )