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 \in V$
	axdc3lem4.2	$⊢ S = \{s \| \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))\}$
	axdc3lem4.3	$⊢ G = (x \in S ⟼ \{y \in S \| (dom y = suc dom x \land {y ↾}_{dom x} = x)\})$
Assertion	axdc3lem4	$⊢ (C \in A \land F : A ⟶ 𝒫 A ∖ \{\emptyset\}) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in F (g (k)))$

Proof

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

Metamath Proof Explorer

Theorem axdc3lem4

Proof