axdc3lem2

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 given the sequence h , we can construct the sequence g that we are after. (Contributed by Mario Carneiro, 30-Jan-2013)

	Ref	Expression
Hypotheses	axdc3lem2.1	$⊢ A \in V$
	axdc3lem2.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)))\}$
	axdc3lem2.3	$⊢ G = (x \in S ⟼ \{y \in S \| (dom y = suc dom x \land {y ↾}_{dom x} = x)\})$
Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		axdc3lem2.1	$⊢ A \in V$
2		axdc3lem2.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		axdc3lem2.3	$⊢ G = (x \in S ⟼ \{y \in S \| (dom y = suc dom x \land {y ↾}_{dom x} = x)\})$
4		id	$⊢ m = \emptyset \to m = \emptyset$
5		fveq2	$⊢ m = \emptyset \to h (m) = h (\emptyset)$
6	5	dmeqd	$⊢ m = \emptyset \to dom h (m) = dom h (\emptyset)$
7	4 6	eleq12d	$⊢ m = \emptyset \to (m \in dom h (m) \leftrightarrow \emptyset \in dom h (\emptyset))$
8		eleq2	$⊢ m = \emptyset \to (j \in m \leftrightarrow j \in \emptyset)$
9	5	sseq2d	$⊢ m = \emptyset \to (h (j) \subseteq h (m) \leftrightarrow h (j) \subseteq h (\emptyset))$
10	8 9	imbi12d	$⊢ m = \emptyset \to ((j \in m \to h (j) \subseteq h (m)) \leftrightarrow (j \in \emptyset \to h (j) \subseteq h (\emptyset)))$
11	7 10	anbi12d	$⊢ m = \emptyset \to ((m \in dom h (m) \land (j \in m \to h (j) \subseteq h (m))) \leftrightarrow (\emptyset \in dom h (\emptyset) \land (j \in \emptyset \to h (j) \subseteq h (\emptyset))))$
12		id	$⊢ m = i \to m = i$
13		fveq2	$⊢ m = i \to h (m) = h (i)$
14	13	dmeqd	$⊢ m = i \to dom h (m) = dom h (i)$
15	12 14	eleq12d	$⊢ m = i \to (m \in dom h (m) \leftrightarrow i \in dom h (i))$
16		elequ2	$⊢ m = i \to (j \in m \leftrightarrow j \in i)$
17	13	sseq2d	$⊢ m = i \to (h (j) \subseteq h (m) \leftrightarrow h (j) \subseteq h (i))$
18	16 17	imbi12d	$⊢ m = i \to ((j \in m \to h (j) \subseteq h (m)) \leftrightarrow (j \in i \to h (j) \subseteq h (i)))$
19	15 18	anbi12d	$⊢ m = i \to ((m \in dom h (m) \land (j \in m \to h (j) \subseteq h (m))) \leftrightarrow (i \in dom h (i) \land (j \in i \to h (j) \subseteq h (i))))$
20		id	$⊢ m = suc i \to m = suc i$
21		fveq2	$⊢ m = suc i \to h (m) = h (suc i)$
22	21	dmeqd	$⊢ m = suc i \to dom h (m) = dom h (suc i)$
23	20 22	eleq12d	$⊢ m = suc i \to (m \in dom h (m) \leftrightarrow suc i \in dom h (suc i))$
24		eleq2	$⊢ m = suc i \to (j \in m \leftrightarrow j \in suc i)$
25	21	sseq2d	$⊢ m = suc i \to (h (j) \subseteq h (m) \leftrightarrow h (j) \subseteq h (suc i))$
26	24 25	imbi12d	$⊢ m = suc i \to ((j \in m \to h (j) \subseteq h (m)) \leftrightarrow (j \in suc i \to h (j) \subseteq h (suc i)))$
27	23 26	anbi12d	$⊢ m = suc i \to ((m \in dom h (m) \land (j \in m \to h (j) \subseteq h (m))) \leftrightarrow (suc i \in dom h (suc i) \land (j \in suc i \to h (j) \subseteq h (suc i))))$
28		peano1	$⊢ \emptyset \in ω$
29		ffvelcdm	$⊢ (h : ω ⟶ S \land \emptyset \in ω) \to h (\emptyset) \in S$
30	28 29	mpan2	$⊢ h : ω ⟶ S \to h (\emptyset) \in S$
31		fdm	$⊢ s : suc n ⟶ A \to dom s = suc n$
32		nnord	$⊢ n \in ω \to Ord n$
33		0elsuc	$⊢ Ord n \to \emptyset \in suc n$
34	32 33	syl	$⊢ n \in ω \to \emptyset \in suc n$
35		peano2	$⊢ n \in ω \to suc n \in ω$
36		eleq2	$⊢ dom s = suc n \to (\emptyset \in dom s \leftrightarrow \emptyset \in suc n)$
37		eleq1	$⊢ dom s = suc n \to (dom s \in ω \leftrightarrow suc n \in ω)$
38	36 37	anbi12d	$⊢ dom s = suc n \to ((\emptyset \in dom s \land dom s \in ω) \leftrightarrow (\emptyset \in suc n \land suc n \in ω))$
39	38	biimprcd	$⊢ (\emptyset \in suc n \land suc n \in ω) \to (dom s = suc n \to (\emptyset \in dom s \land dom s \in ω))$
40	34 35 39	syl2anc	$⊢ n \in ω \to (dom s = suc n \to (\emptyset \in dom s \land dom s \in ω))$
41	31 40	syl5com	$⊢ s : suc n ⟶ A \to (n \in ω \to (\emptyset \in dom s \land dom s \in ω))$
42	41	3ad2ant1	$⊢ (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to (n \in ω \to (\emptyset \in dom s \land dom s \in ω))$
43	42	impcom	$⊢ (n \in ω \land (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))) \to (\emptyset \in dom s \land dom s \in ω)$
44	43	rexlimiva	$⊢ \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to (\emptyset \in dom s \land dom s \in ω)$
45	44	ss2abi	$⊢ \{s \| \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))\} \subseteq \{s \| (\emptyset \in dom s \land dom s \in ω)\}$
46	2 45	eqsstri	$⊢ S \subseteq \{s \| (\emptyset \in dom s \land dom s \in ω)\}$
47	46	sseli	$⊢ h (\emptyset) \in S \to h (\emptyset) \in \{s \| (\emptyset \in dom s \land dom s \in ω)\}$
48		fvex	$⊢ h (\emptyset) \in V$
49		dmeq	$⊢ s = h (\emptyset) \to dom s = dom h (\emptyset)$
50	49	eleq2d	$⊢ s = h (\emptyset) \to (\emptyset \in dom s \leftrightarrow \emptyset \in dom h (\emptyset))$
51	49	eleq1d	$⊢ s = h (\emptyset) \to (dom s \in ω \leftrightarrow dom h (\emptyset) \in ω)$
52	50 51	anbi12d	$⊢ s = h (\emptyset) \to ((\emptyset \in dom s \land dom s \in ω) \leftrightarrow (\emptyset \in dom h (\emptyset) \land dom h (\emptyset) \in ω))$
53	48 52	elab	$⊢ h (\emptyset) \in \{s \| (\emptyset \in dom s \land dom s \in ω)\} \leftrightarrow (\emptyset \in dom h (\emptyset) \land dom h (\emptyset) \in ω)$
54	47 53	sylib	$⊢ h (\emptyset) \in S \to (\emptyset \in dom h (\emptyset) \land dom h (\emptyset) \in ω)$
55	54	simpld	$⊢ h (\emptyset) \in S \to \emptyset \in dom h (\emptyset)$
56	30 55	syl	$⊢ h : ω ⟶ S \to \emptyset \in dom h (\emptyset)$
57		noel	$⊢ \neg j \in \emptyset$
58	57	pm2.21i	$⊢ j \in \emptyset \to h (j) \subseteq h (\emptyset)$
59	56 58	jctir	$⊢ h : ω ⟶ S \to (\emptyset \in dom h (\emptyset) \land (j \in \emptyset \to h (j) \subseteq h (\emptyset)))$
60	59	adantr	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (\emptyset \in dom h (\emptyset) \land (j \in \emptyset \to h (j) \subseteq h (\emptyset)))$
61		ffvelcdm	$⊢ (h : ω ⟶ S \land i \in ω) \to h (i) \in S$
62	61	ancoms	$⊢ (i \in ω \land h : ω ⟶ S) \to h (i) \in S$
63	62	adantrr	$⊢ (i \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to h (i) \in S$
64		suceq	$⊢ k = i \to suc k = suc i$
65	64	fveq2d	$⊢ k = i \to h (suc k) = h (suc i)$
66		2fveq3	$⊢ k = i \to G (h (k)) = G (h (i))$
67	65 66	eleq12d	$⊢ k = i \to (h (suc k) \in G (h (k)) \leftrightarrow h (suc i) \in G (h (i)))$
68	67	rspcva	$⊢ (i \in ω \land \forall k \in ω h (suc k) \in G (h (k))) \to h (suc i) \in G (h (i))$
69	68	adantrl	$⊢ (i \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to h (suc i) \in G (h (i))$
70	46	sseli	$⊢ h (i) \in S \to h (i) \in \{s \| (\emptyset \in dom s \land dom s \in ω)\}$
71		fvex	$⊢ h (i) \in V$
72		dmeq	$⊢ s = h (i) \to dom s = dom h (i)$
73	72	eleq2d	$⊢ s = h (i) \to (\emptyset \in dom s \leftrightarrow \emptyset \in dom h (i))$
74	72	eleq1d	$⊢ s = h (i) \to (dom s \in ω \leftrightarrow dom h (i) \in ω)$
75	73 74	anbi12d	$⊢ s = h (i) \to ((\emptyset \in dom s \land dom s \in ω) \leftrightarrow (\emptyset \in dom h (i) \land dom h (i) \in ω))$
76	71 75	elab	$⊢ h (i) \in \{s \| (\emptyset \in dom s \land dom s \in ω)\} \leftrightarrow (\emptyset \in dom h (i) \land dom h (i) \in ω)$
77	70 76	sylib	$⊢ h (i) \in S \to (\emptyset \in dom h (i) \land dom h (i) \in ω)$
78	77	simprd	$⊢ h (i) \in S \to dom h (i) \in ω$
79		nnord	$⊢ dom h (i) \in ω \to Ord dom h (i)$
80		ordsucelsuc	$⊢ Ord dom h (i) \to (i \in dom h (i) \leftrightarrow suc i \in suc dom h (i))$
81	78 79 80	3syl	$⊢ h (i) \in S \to (i \in dom h (i) \leftrightarrow suc i \in suc dom h (i))$
82	81	adantr	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to (i \in dom h (i) \leftrightarrow suc i \in suc dom h (i))$
83		dmeq	$⊢ x = h (i) \to dom x = dom h (i)$
84		suceq	$⊢ dom x = dom h (i) \to suc dom x = suc dom h (i)$
85	83 84	syl	$⊢ x = h (i) \to suc dom x = suc dom h (i)$
86	85	eqeq2d	$⊢ x = h (i) \to (dom y = suc dom x \leftrightarrow dom y = suc dom h (i))$
87	83	reseq2d	$⊢ x = h (i) \to {y ↾}_{dom x} = {y ↾}_{dom h (i)}$
88		id	$⊢ x = h (i) \to x = h (i)$
89	87 88	eqeq12d	$⊢ x = h (i) \to ({y ↾}_{dom x} = x \leftrightarrow {y ↾}_{dom h (i)} = h (i))$
90	86 89	anbi12d	$⊢ x = h (i) \to ((dom y = suc dom x \land {y ↾}_{dom x} = x) \leftrightarrow (dom y = suc dom h (i) \land {y ↾}_{dom h (i)} = h (i)))$
91	90	rabbidv	$⊢ x = h (i) \to \{y \in S \| (dom y = suc dom x \land {y ↾}_{dom x} = x)\} = \{y \in S \| (dom y = suc dom h (i) \land {y ↾}_{dom h (i)} = h (i))\}$
92	1 2	axdc3lem	$⊢ S \in V$
93	92	rabex	$⊢ \{y \in S \| (dom y = suc dom h (i) \land {y ↾}_{dom h (i)} = h (i))\} \in V$
94	91 3 93	fvmpt	$⊢ h (i) \in S \to G (h (i)) = \{y \in S \| (dom y = suc dom h (i) \land {y ↾}_{dom h (i)} = h (i))\}$
95	94	eleq2d	$⊢ h (i) \in S \to (h (suc i) \in G (h (i)) \leftrightarrow h (suc i) \in \{y \in S \| (dom y = suc dom h (i) \land {y ↾}_{dom h (i)} = h (i))\})$
96		dmeq	$⊢ y = h (suc i) \to dom y = dom h (suc i)$
97	96	eqeq1d	$⊢ y = h (suc i) \to (dom y = suc dom h (i) \leftrightarrow dom h (suc i) = suc dom h (i))$
98		reseq1	$⊢ y = h (suc i) \to {y ↾}_{dom h (i)} = {h (suc i) ↾}_{dom h (i)}$
99	98	eqeq1d	$⊢ y = h (suc i) \to ({y ↾}_{dom h (i)} = h (i) \leftrightarrow {h (suc i) ↾}_{dom h (i)} = h (i))$
100	97 99	anbi12d	$⊢ y = h (suc i) \to ((dom y = suc dom h (i) \land {y ↾}_{dom h (i)} = h (i)) \leftrightarrow (dom h (suc i) = suc dom h (i) \land {h (suc i) ↾}_{dom h (i)} = h (i)))$
101	100	elrab	$⊢ h (suc i) \in \{y \in S \| (dom y = suc dom h (i) \land {y ↾}_{dom h (i)} = h (i))\} \leftrightarrow (h (suc i) \in S \land (dom h (suc i) = suc dom h (i) \land {h (suc i) ↾}_{dom h (i)} = h (i)))$
102	95 101	bitrdi	$⊢ h (i) \in S \to (h (suc i) \in G (h (i)) \leftrightarrow (h (suc i) \in S \land (dom h (suc i) = suc dom h (i) \land {h (suc i) ↾}_{dom h (i)} = h (i))))$
103	102	simplbda	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to (dom h (suc i) = suc dom h (i) \land {h (suc i) ↾}_{dom h (i)} = h (i))$
104	103	simpld	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to dom h (suc i) = suc dom h (i)$
105	104	eleq2d	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to (suc i \in dom h (suc i) \leftrightarrow suc i \in suc dom h (i))$
106	82 105	bitr4d	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to (i \in dom h (i) \leftrightarrow suc i \in dom h (suc i))$
107	106	biimpd	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to (i \in dom h (i) \to suc i \in dom h (suc i))$
108	103	simprd	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to {h (suc i) ↾}_{dom h (i)} = h (i)$
109		resss	$⊢ {h (suc i) ↾}_{dom h (i)} \subseteq h (suc i)$
110		sseq1	$⊢ {h (suc i) ↾}_{dom h (i)} = h (i) \to ({h (suc i) ↾}_{dom h (i)} \subseteq h (suc i) \leftrightarrow h (i) \subseteq h (suc i))$
111	109 110	mpbii	$⊢ {h (suc i) ↾}_{dom h (i)} = h (i) \to h (i) \subseteq h (suc i)$
112		elsuci	$⊢ j \in suc i \to (j \in i \lor j = i)$
113		pm2.27	$⊢ j \in i \to ((j \in i \to h (j) \subseteq h (i)) \to h (j) \subseteq h (i))$
114		sstr2	$⊢ h (j) \subseteq h (i) \to (h (i) \subseteq h (suc i) \to h (j) \subseteq h (suc i))$
115	113 114	syl6	$⊢ j \in i \to ((j \in i \to h (j) \subseteq h (i)) \to (h (i) \subseteq h (suc i) \to h (j) \subseteq h (suc i)))$
116		fveq2	$⊢ j = i \to h (j) = h (i)$
117	116	sseq1d	$⊢ j = i \to (h (j) \subseteq h (suc i) \leftrightarrow h (i) \subseteq h (suc i))$
118	117	biimprd	$⊢ j = i \to (h (i) \subseteq h (suc i) \to h (j) \subseteq h (suc i))$
119	118	a1d	$⊢ j = i \to ((j \in i \to h (j) \subseteq h (i)) \to (h (i) \subseteq h (suc i) \to h (j) \subseteq h (suc i)))$
120	115 119	jaoi	$⊢ (j \in i \lor j = i) \to ((j \in i \to h (j) \subseteq h (i)) \to (h (i) \subseteq h (suc i) \to h (j) \subseteq h (suc i)))$
121	112 120	syl	$⊢ j \in suc i \to ((j \in i \to h (j) \subseteq h (i)) \to (h (i) \subseteq h (suc i) \to h (j) \subseteq h (suc i)))$
122	121	com13	$⊢ h (i) \subseteq h (suc i) \to ((j \in i \to h (j) \subseteq h (i)) \to (j \in suc i \to h (j) \subseteq h (suc i)))$
123	108 111 122	3syl	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to ((j \in i \to h (j) \subseteq h (i)) \to (j \in suc i \to h (j) \subseteq h (suc i)))$
124	107 123	anim12d	$⊢ (h (i) \in S \land h (suc i) \in G (h (i))) \to ((i \in dom h (i) \land (j \in i \to h (j) \subseteq h (i))) \to (suc i \in dom h (suc i) \land (j \in suc i \to h (j) \subseteq h (suc i))))$
125	63 69 124	syl2anc	$⊢ (i \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to ((i \in dom h (i) \land (j \in i \to h (j) \subseteq h (i))) \to (suc i \in dom h (suc i) \land (j \in suc i \to h (j) \subseteq h (suc i))))$
126	125	ex	$⊢ i \in ω \to ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to ((i \in dom h (i) \land (j \in i \to h (j) \subseteq h (i))) \to (suc i \in dom h (suc i) \land (j \in suc i \to h (j) \subseteq h (suc i)))))$
127	11 19 27 60 126	finds2	$⊢ m \in ω \to ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (m \in dom h (m) \land (j \in m \to h (j) \subseteq h (m))))$
128	127	imp	$⊢ (m \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to (m \in dom h (m) \land (j \in m \to h (j) \subseteq h (m)))$
129	128	simprd	$⊢ (m \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to (j \in m \to h (j) \subseteq h (m))$
130	129	expcom	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (m \in ω \to (j \in m \to h (j) \subseteq h (m)))$
131	130	ralrimdv	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (m \in ω \to \forall j \in m h (j) \subseteq h (m))$
132	131	ralrimiv	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to \forall m \in ω \forall j \in m h (j) \subseteq h (m)$
133		frn	$⊢ h : ω ⟶ S \to ran h \subseteq S$
134		ffun	$⊢ s : suc n ⟶ A \to Fun s$
135	134	3ad2ant1	$⊢ (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to Fun s$
136	135	rexlimivw	$⊢ \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to Fun s$
137	136	ss2abi	$⊢ \{s \| \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))\} \subseteq \{s \| Fun s\}$
138	2 137	eqsstri	$⊢ S \subseteq \{s \| Fun s\}$
139	133 138	sstrdi	$⊢ h : ω ⟶ S \to ran h \subseteq \{s \| Fun s\}$
140	139	sseld	$⊢ h : ω ⟶ S \to (u \in ran h \to u \in \{s \| Fun s\})$
141		vex	$⊢ u \in V$
142		funeq	$⊢ s = u \to (Fun s \leftrightarrow Fun u)$
143	141 142	elab	$⊢ u \in \{s \| Fun s\} \leftrightarrow Fun u$
144	140 143	imbitrdi	$⊢ h : ω ⟶ S \to (u \in ran h \to Fun u)$
145	144	adantr	$⊢ (h : ω ⟶ S \land \forall m \in ω \forall j \in m h (j) \subseteq h (m)) \to (u \in ran h \to Fun u)$
146		ffn	$⊢ h : ω ⟶ S \to h Fn ω$
147		fvelrnb	$⊢ h Fn ω \to (v \in ran h \leftrightarrow \exists b \in ω h (b) = v)$
148		fvelrnb	$⊢ h Fn ω \to (u \in ran h \leftrightarrow \exists a \in ω h (a) = u)$
149		nnord	$⊢ a \in ω \to Ord a$
150		nnord	$⊢ b \in ω \to Ord b$
151	149 150	anim12i	$⊢ (a \in ω \land b \in ω) \to (Ord a \land Ord b)$
152		ordtri3or	$⊢ (Ord a \land Ord b) \to (a \in b \lor a = b \lor b \in a)$
153		fveq2	$⊢ m = b \to h (m) = h (b)$
154	153	sseq2d	$⊢ m = b \to (h (j) \subseteq h (m) \leftrightarrow h (j) \subseteq h (b))$
155	154	raleqbi1dv	$⊢ m = b \to (\forall j \in m h (j) \subseteq h (m) \leftrightarrow \forall j \in b h (j) \subseteq h (b))$
156	155	rspcv	$⊢ b \in ω \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to \forall j \in b h (j) \subseteq h (b))$
157		fveq2	$⊢ j = a \to h (j) = h (a)$
158	157	sseq1d	$⊢ j = a \to (h (j) \subseteq h (b) \leftrightarrow h (a) \subseteq h (b))$
159	158	rspccv	$⊢ \forall j \in b h (j) \subseteq h (b) \to (a \in b \to h (a) \subseteq h (b))$
160	156 159	syl6	$⊢ b \in ω \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (a \in b \to h (a) \subseteq h (b)))$
161	160	adantl	$⊢ (a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (a \in b \to h (a) \subseteq h (b)))$
162	161	3imp	$⊢ ((a \in ω \land b \in ω) \land \forall m \in ω \forall j \in m h (j) \subseteq h (m) \land a \in b) \to h (a) \subseteq h (b)$
163	162	orcd	$⊢ ((a \in ω \land b \in ω) \land \forall m \in ω \forall j \in m h (j) \subseteq h (m) \land a \in b) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))$
164	163	3exp	$⊢ (a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (a \in b \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))))$
165	164	com3r	$⊢ a \in b \to ((a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))))$
166		fveq2	$⊢ a = b \to h (a) = h (b)$
167		eqimss	$⊢ h (a) = h (b) \to h (a) \subseteq h (b)$
168	167	orcd	$⊢ h (a) = h (b) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))$
169	166 168	syl	$⊢ a = b \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))$
170	169	2a1d	$⊢ a = b \to ((a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))))$
171		fveq2	$⊢ m = a \to h (m) = h (a)$
172	171	sseq2d	$⊢ m = a \to (h (j) \subseteq h (m) \leftrightarrow h (j) \subseteq h (a))$
173	172	raleqbi1dv	$⊢ m = a \to (\forall j \in m h (j) \subseteq h (m) \leftrightarrow \forall j \in a h (j) \subseteq h (a))$
174	173	rspcv	$⊢ a \in ω \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to \forall j \in a h (j) \subseteq h (a))$
175		fveq2	$⊢ j = b \to h (j) = h (b)$
176	175	sseq1d	$⊢ j = b \to (h (j) \subseteq h (a) \leftrightarrow h (b) \subseteq h (a))$
177	176	rspccv	$⊢ \forall j \in a h (j) \subseteq h (a) \to (b \in a \to h (b) \subseteq h (a))$
178	174 177	syl6	$⊢ a \in ω \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (b \in a \to h (b) \subseteq h (a)))$
179	178	adantr	$⊢ (a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (b \in a \to h (b) \subseteq h (a)))$
180	179	3imp	$⊢ ((a \in ω \land b \in ω) \land \forall m \in ω \forall j \in m h (j) \subseteq h (m) \land b \in a) \to h (b) \subseteq h (a)$
181	180	olcd	$⊢ ((a \in ω \land b \in ω) \land \forall m \in ω \forall j \in m h (j) \subseteq h (m) \land b \in a) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))$
182	181	3exp	$⊢ (a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (b \in a \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))))$
183	182	com3r	$⊢ b \in a \to ((a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))))$
184	165 170 183	3jaoi	$⊢ (a \in b \lor a = b \lor b \in a) \to ((a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))))$
185	152 184	syl	$⊢ (Ord a \land Ord b) \to ((a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a))))$
186	151 185	mpcom	$⊢ (a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (h (a) \subseteq h (b) \lor h (b) \subseteq h (a)))$
187		sseq12	$⊢ (h (a) = u \land h (b) = v) \to (h (a) \subseteq h (b) \leftrightarrow u \subseteq v)$
188		sseq12	$⊢ (h (b) = v \land h (a) = u) \to (h (b) \subseteq h (a) \leftrightarrow v \subseteq u)$
189	188	ancoms	$⊢ (h (a) = u \land h (b) = v) \to (h (b) \subseteq h (a) \leftrightarrow v \subseteq u)$
190	187 189	orbi12d	$⊢ (h (a) = u \land h (b) = v) \to ((h (a) \subseteq h (b) \lor h (b) \subseteq h (a)) \leftrightarrow (u \subseteq v \lor v \subseteq u))$
191	190	biimpcd	$⊢ (h (a) \subseteq h (b) \lor h (b) \subseteq h (a)) \to ((h (a) = u \land h (b) = v) \to (u \subseteq v \lor v \subseteq u))$
192	186 191	syl6	$⊢ (a \in ω \land b \in ω) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to ((h (a) = u \land h (b) = v) \to (u \subseteq v \lor v \subseteq u)))$
193	192	com23	$⊢ (a \in ω \land b \in ω) \to ((h (a) = u \land h (b) = v) \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u)))$
194	193	exp4b	$⊢ a \in ω \to (b \in ω \to (h (a) = u \to (h (b) = v \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u)))))$
195	194	com23	$⊢ a \in ω \to (h (a) = u \to (b \in ω \to (h (b) = v \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u)))))$
196	195	rexlimiv	$⊢ \exists a \in ω h (a) = u \to (b \in ω \to (h (b) = v \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u))))$
197	196	rexlimdv	$⊢ \exists a \in ω h (a) = u \to (\exists b \in ω h (b) = v \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u)))$
198	148 197	syl6bi	$⊢ h Fn ω \to (u \in ran h \to (\exists b \in ω h (b) = v \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u))))$
199	198	com23	$⊢ h Fn ω \to (\exists b \in ω h (b) = v \to (u \in ran h \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u))))$
200	147 199	sylbid	$⊢ h Fn ω \to (v \in ran h \to (u \in ran h \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \subseteq v \lor v \subseteq u))))$
201	200	com24	$⊢ h Fn ω \to (\forall m \in ω \forall j \in m h (j) \subseteq h (m) \to (u \in ran h \to (v \in ran h \to (u \subseteq v \lor v \subseteq u))))$
202	201	imp	$⊢ (h Fn ω \land \forall m \in ω \forall j \in m h (j) \subseteq h (m)) \to (u \in ran h \to (v \in ran h \to (u \subseteq v \lor v \subseteq u)))$
203	202	ralrimdv	$⊢ (h Fn ω \land \forall m \in ω \forall j \in m h (j) \subseteq h (m)) \to (u \in ran h \to \forall v \in ran h (u \subseteq v \lor v \subseteq u))$
204	146 203	sylan	$⊢ (h : ω ⟶ S \land \forall m \in ω \forall j \in m h (j) \subseteq h (m)) \to (u \in ran h \to \forall v \in ran h (u \subseteq v \lor v \subseteq u))$
205	145 204	jcad	$⊢ (h : ω ⟶ S \land \forall m \in ω \forall j \in m h (j) \subseteq h (m)) \to (u \in ran h \to (Fun u \land \forall v \in ran h (u \subseteq v \lor v \subseteq u)))$
206	205	ralrimiv	$⊢ (h : ω ⟶ S \land \forall m \in ω \forall j \in m h (j) \subseteq h (m)) \to \forall u \in ran h (Fun u \land \forall v \in ran h (u \subseteq v \lor v \subseteq u))$
207		fununi	$⊢ \forall u \in ran h (Fun u \land \forall v \in ran h (u \subseteq v \lor v \subseteq u)) \to Fun ⋃ ran h$
208	206 207	syl	$⊢ (h : ω ⟶ S \land \forall m \in ω \forall j \in m h (j) \subseteq h (m)) \to Fun ⋃ ran h$
209	132 208	syldan	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to Fun ⋃ ran h$
210		vex	$⊢ m \in V$
211	210	eldm2	$⊢ m \in dom ⋃ ran h \leftrightarrow \exists u ⟨m, u⟩ \in ⋃ ran h$
212		eluni2	$⊢ ⟨m, u⟩ \in ⋃ ran h \leftrightarrow \exists v \in ran h ⟨m, u⟩ \in v$
213	210 141	opeldm	$⊢ ⟨m, u⟩ \in v \to m \in dom v$
214	213	a1i	$⊢ h : ω ⟶ S \to (⟨m, u⟩ \in v \to m \in dom v)$
215	133 46	sstrdi	$⊢ h : ω ⟶ S \to ran h \subseteq \{s \| (\emptyset \in dom s \land dom s \in ω)\}$
216		ssel	$⊢ ran h \subseteq \{s \| (\emptyset \in dom s \land dom s \in ω)\} \to (v \in ran h \to v \in \{s \| (\emptyset \in dom s \land dom s \in ω)\})$
217		vex	$⊢ v \in V$
218		dmeq	$⊢ s = v \to dom s = dom v$
219	218	eleq2d	$⊢ s = v \to (\emptyset \in dom s \leftrightarrow \emptyset \in dom v)$
220	218	eleq1d	$⊢ s = v \to (dom s \in ω \leftrightarrow dom v \in ω)$
221	219 220	anbi12d	$⊢ s = v \to ((\emptyset \in dom s \land dom s \in ω) \leftrightarrow (\emptyset \in dom v \land dom v \in ω))$
222	217 221	elab	$⊢ v \in \{s \| (\emptyset \in dom s \land dom s \in ω)\} \leftrightarrow (\emptyset \in dom v \land dom v \in ω)$
223	222	simprbi	$⊢ v \in \{s \| (\emptyset \in dom s \land dom s \in ω)\} \to dom v \in ω$
224	216 223	syl6	$⊢ ran h \subseteq \{s \| (\emptyset \in dom s \land dom s \in ω)\} \to (v \in ran h \to dom v \in ω)$
225	215 224	syl	$⊢ h : ω ⟶ S \to (v \in ran h \to dom v \in ω)$
226	214 225	anim12d	$⊢ h : ω ⟶ S \to ((⟨m, u⟩ \in v \land v \in ran h) \to (m \in dom v \land dom v \in ω))$
227		elnn	$⊢ (m \in dom v \land dom v \in ω) \to m \in ω$
228	226 227	syl6	$⊢ h : ω ⟶ S \to ((⟨m, u⟩ \in v \land v \in ran h) \to m \in ω)$
229	228	expcomd	$⊢ h : ω ⟶ S \to (v \in ran h \to (⟨m, u⟩ \in v \to m \in ω))$
230	229	rexlimdv	$⊢ h : ω ⟶ S \to (\exists v \in ran h ⟨m, u⟩ \in v \to m \in ω)$
231	212 230	biimtrid	$⊢ h : ω ⟶ S \to (⟨m, u⟩ \in ⋃ ran h \to m \in ω)$
232	231	exlimdv	$⊢ h : ω ⟶ S \to (\exists u ⟨m, u⟩ \in ⋃ ran h \to m \in ω)$
233	211 232	biimtrid	$⊢ h : ω ⟶ S \to (m \in dom ⋃ ran h \to m \in ω)$
234	233	adantr	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (m \in dom ⋃ ran h \to m \in ω)$
235		id	$⊢ m \in ω \to m \in ω$
236		fnfvelrn	$⊢ (h Fn ω \land m \in ω) \to h (m) \in ran h$
237	146 235 236	syl2anr	$⊢ (m \in ω \land h : ω ⟶ S) \to h (m) \in ran h$
238	237	adantrr	$⊢ (m \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to h (m) \in ran h$
239	128	simpld	$⊢ (m \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to m \in dom h (m)$
240		dmeq	$⊢ u = h (m) \to dom u = dom h (m)$
241	240	eliuni	$⊢ (h (m) \in ran h \land m \in dom h (m)) \to m \in ⋃_{u \in ran h} dom u$
242	238 239 241	syl2anc	$⊢ (m \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to m \in ⋃_{u \in ran h} dom u$
243		dmuni	$⊢ dom ⋃ ran h = ⋃_{u \in ran h} dom u$
244	242 243	eleqtrrdi	$⊢ (m \in ω \land (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))) \to m \in dom ⋃ ran h$
245	244	expcom	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (m \in ω \to m \in dom ⋃ ran h)$
246	234 245	impbid	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (m \in dom ⋃ ran h \leftrightarrow m \in ω)$
247	246	eqrdv	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to dom ⋃ ran h = ω$
248		rnuni	$⊢ ran ⋃ ran h = ⋃_{s \in ran h} ran s$
249		frn	$⊢ s : suc n ⟶ A \to ran s \subseteq A$
250	249	3ad2ant1	$⊢ (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to ran s \subseteq A$
251	250	rexlimivw	$⊢ \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to ran s \subseteq A$
252	251	ss2abi	$⊢ \{s \| \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))\} \subseteq \{s \| ran s \subseteq A\}$
253	2 252	eqsstri	$⊢ S \subseteq \{s \| ran s \subseteq A\}$
254	133 253	sstrdi	$⊢ h : ω ⟶ S \to ran h \subseteq \{s \| ran s \subseteq A\}$
255		ssel	$⊢ ran h \subseteq \{s \| ran s \subseteq A\} \to (s \in ran h \to s \in \{s \| ran s \subseteq A\})$
256		abid	$⊢ s \in \{s \| ran s \subseteq A\} \leftrightarrow ran s \subseteq A$
257	255 256	imbitrdi	$⊢ ran h \subseteq \{s \| ran s \subseteq A\} \to (s \in ran h \to ran s \subseteq A)$
258	254 257	syl	$⊢ h : ω ⟶ S \to (s \in ran h \to ran s \subseteq A)$
259	258	ralrimiv	$⊢ h : ω ⟶ S \to \forall s \in ran h ran s \subseteq A$
260		iunss	$⊢ ⋃_{s \in ran h} ran s \subseteq A \leftrightarrow \forall s \in ran h ran s \subseteq A$
261	259 260	sylibr	$⊢ h : ω ⟶ S \to ⋃_{s \in ran h} ran s \subseteq A$
262	248 261	eqsstrid	$⊢ h : ω ⟶ S \to ran ⋃ ran h \subseteq A$
263	262	adantr	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to ran ⋃ ran h \subseteq A$
264		df-fn	$⊢ ⋃ ran h Fn ω \leftrightarrow (Fun ⋃ ran h \land dom ⋃ ran h = ω)$
265		df-f	$⊢ ⋃ ran h : ω ⟶ A \leftrightarrow (⋃ ran h Fn ω \land ran ⋃ ran h \subseteq A)$
266	265	biimpri	$⊢ (⋃ ran h Fn ω \land ran ⋃ ran h \subseteq A) \to ⋃ ran h : ω ⟶ A$
267	264 266	sylanbr	$⊢ ((Fun ⋃ ran h \land dom ⋃ ran h = ω) \land ran ⋃ ran h \subseteq A) \to ⋃ ran h : ω ⟶ A$
268	209 247 263 267	syl21anc	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to ⋃ ran h : ω ⟶ A$
269		fnfvelrn	$⊢ (h Fn ω \land \emptyset \in ω) \to h (\emptyset) \in ran h$
270	146 28 269	sylancl	$⊢ h : ω ⟶ S \to h (\emptyset) \in ran h$
271	270	adantr	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to h (\emptyset) \in ran h$
272		elssuni	$⊢ h (\emptyset) \in ran h \to h (\emptyset) \subseteq ⋃ ran h$
273	271 272	syl	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to h (\emptyset) \subseteq ⋃ ran h$
274	56	adantr	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to \emptyset \in dom h (\emptyset)$
275		funssfv	$⊢ (Fun ⋃ ran h \land h (\emptyset) \subseteq ⋃ ran h \land \emptyset \in dom h (\emptyset)) \to ⋃ ran h (\emptyset) = h (\emptyset) (\emptyset)$
276	209 273 274 275	syl3anc	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to ⋃ ran h (\emptyset) = h (\emptyset) (\emptyset)$
277		simp2	$⊢ (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to s (\emptyset) = C$
278	277	rexlimivw	$⊢ \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to s (\emptyset) = C$
279	278	ss2abi	$⊢ \{s \| \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))\} \subseteq \{s \| s (\emptyset) = C\}$
280	2 279	eqsstri	$⊢ S \subseteq \{s \| s (\emptyset) = C\}$
281	133 280	sstrdi	$⊢ h : ω ⟶ S \to ran h \subseteq \{s \| s (\emptyset) = C\}$
282		ssel	$⊢ ran h \subseteq \{s \| s (\emptyset) = C\} \to (h (\emptyset) \in ran h \to h (\emptyset) \in \{s \| s (\emptyset) = C\})$
283		fveq1	$⊢ s = h (\emptyset) \to s (\emptyset) = h (\emptyset) (\emptyset)$
284	283	eqeq1d	$⊢ s = h (\emptyset) \to (s (\emptyset) = C \leftrightarrow h (\emptyset) (\emptyset) = C)$
285	48 284	elab	$⊢ h (\emptyset) \in \{s \| s (\emptyset) = C\} \leftrightarrow h (\emptyset) (\emptyset) = C$
286	282 285	imbitrdi	$⊢ ran h \subseteq \{s \| s (\emptyset) = C\} \to (h (\emptyset) \in ran h \to h (\emptyset) (\emptyset) = C)$
287	281 286	syl	$⊢ h : ω ⟶ S \to (h (\emptyset) \in ran h \to h (\emptyset) (\emptyset) = C)$
288	287	adantr	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (h (\emptyset) \in ran h \to h (\emptyset) (\emptyset) = C)$
289	271 288	mpd	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to h (\emptyset) (\emptyset) = C$
290	276 289	eqtrd	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to ⋃ ran h (\emptyset) = C$
291		nfv	$⊢ Ⅎ k h : ω ⟶ S$
292		nfra1	$⊢ Ⅎ k \forall k \in ω h (suc k) \in G (h (k))$
293	291 292	nfan	$⊢ Ⅎ k (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k)))$
294	133	ad2antrr	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to ran h \subseteq S$
295		peano2	$⊢ k \in ω \to suc k \in ω$
296		fnfvelrn	$⊢ (h Fn ω \land suc k \in ω) \to h (suc k) \in ran h$
297	146 295 296	syl2an	$⊢ (h : ω ⟶ S \land k \in ω) \to h (suc k) \in ran h$
298	297	adantlr	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to h (suc k) \in ran h$
299	239	expcom	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (m \in ω \to m \in dom h (m))$
300	299	ralrimiv	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to \forall m \in ω m \in dom h (m)$
301		id	$⊢ m = suc k \to m = suc k$
302		fveq2	$⊢ m = suc k \to h (m) = h (suc k)$
303	302	dmeqd	$⊢ m = suc k \to dom h (m) = dom h (suc k)$
304	301 303	eleq12d	$⊢ m = suc k \to (m \in dom h (m) \leftrightarrow suc k \in dom h (suc k))$
305	304	rspcv	$⊢ suc k \in ω \to (\forall m \in ω m \in dom h (m) \to suc k \in dom h (suc k))$
306	295 305	syl	$⊢ k \in ω \to (\forall m \in ω m \in dom h (m) \to suc k \in dom h (suc k))$
307	300 306	mpan9	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to suc k \in dom h (suc k)$
308		eleq2	$⊢ dom s = suc n \to (suc k \in dom s \leftrightarrow suc k \in suc n)$
309	308	biimpa	$⊢ (dom s = suc n \land suc k \in dom s) \to suc k \in suc n$
310	31 309	sylan	$⊢ (s : suc n ⟶ A \land suc k \in dom s) \to suc k \in suc n$
311		ordsucelsuc	$⊢ Ord n \to (k \in n \leftrightarrow suc k \in suc n)$
312	32 311	syl	$⊢ n \in ω \to (k \in n \leftrightarrow suc k \in suc n)$
313	312	biimprd	$⊢ n \in ω \to (suc k \in suc n \to k \in n)$
314		rsp	$⊢ \forall k \in n s (suc k) \in F (s (k)) \to (k \in n \to s (suc k) \in F (s (k)))$
315	313 314	syl9r	$⊢ \forall k \in n s (suc k) \in F (s (k)) \to (n \in ω \to (suc k \in suc n \to s (suc k) \in F (s (k))))$
316	315	com13	$⊢ suc k \in suc n \to (n \in ω \to (\forall k \in n s (suc k) \in F (s (k)) \to s (suc k) \in F (s (k))))$
317	310 316	syl	$⊢ (s : suc n ⟶ A \land suc k \in dom s) \to (n \in ω \to (\forall k \in n s (suc k) \in F (s (k)) \to s (suc k) \in F (s (k))))$
318	317	ex	$⊢ s : suc n ⟶ A \to (suc k \in dom s \to (n \in ω \to (\forall k \in n s (suc k) \in F (s (k)) \to s (suc k) \in F (s (k)))))$
319	318	com24	$⊢ s : suc n ⟶ A \to (\forall k \in n s (suc k) \in F (s (k)) \to (n \in ω \to (suc k \in dom s \to s (suc k) \in F (s (k)))))$
320	319	imp	$⊢ (s : suc n ⟶ A \land \forall k \in n s (suc k) \in F (s (k))) \to (n \in ω \to (suc k \in dom s \to s (suc k) \in F (s (k))))$
321	320	3adant2	$⊢ (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to (n \in ω \to (suc k \in dom s \to s (suc k) \in F (s (k))))$
322	321	impcom	$⊢ (n \in ω \land (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))) \to (suc k \in dom s \to s (suc k) \in F (s (k)))$
323	322	rexlimiva	$⊢ \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k))) \to (suc k \in dom s \to s (suc k) \in F (s (k)))$
324	323	ss2abi	$⊢ \{s \| \exists n \in ω (s : suc n ⟶ A \land s (\emptyset) = C \land \forall k \in n s (suc k) \in F (s (k)))\} \subseteq \{s \| (suc k \in dom s \to s (suc k) \in F (s (k)))\}$
325	2 324	eqsstri	$⊢ S \subseteq \{s \| (suc k \in dom s \to s (suc k) \in F (s (k)))\}$
326		sstr	$⊢ (ran h \subseteq S \land S \subseteq \{s \| (suc k \in dom s \to s (suc k) \in F (s (k)))\}) \to ran h \subseteq \{s \| (suc k \in dom s \to s (suc k) \in F (s (k)))\}$
327	325 326	mpan2	$⊢ ran h \subseteq S \to ran h \subseteq \{s \| (suc k \in dom s \to s (suc k) \in F (s (k)))\}$
328	327	sseld	$⊢ ran h \subseteq S \to (h (suc k) \in ran h \to h (suc k) \in \{s \| (suc k \in dom s \to s (suc k) \in F (s (k)))\})$
329		fvex	$⊢ h (suc k) \in V$
330		dmeq	$⊢ s = h (suc k) \to dom s = dom h (suc k)$
331	330	eleq2d	$⊢ s = h (suc k) \to (suc k \in dom s \leftrightarrow suc k \in dom h (suc k))$
332		fveq1	$⊢ s = h (suc k) \to s (suc k) = h (suc k) (suc k)$
333		fveq1	$⊢ s = h (suc k) \to s (k) = h (suc k) (k)$
334	333	fveq2d	$⊢ s = h (suc k) \to F (s (k)) = F (h (suc k) (k))$
335	332 334	eleq12d	$⊢ s = h (suc k) \to (s (suc k) \in F (s (k)) \leftrightarrow h (suc k) (suc k) \in F (h (suc k) (k)))$
336	331 335	imbi12d	$⊢ s = h (suc k) \to ((suc k \in dom s \to s (suc k) \in F (s (k))) \leftrightarrow (suc k \in dom h (suc k) \to h (suc k) (suc k) \in F (h (suc k) (k))))$
337	329 336	elab	$⊢ h (suc k) \in \{s \| (suc k \in dom s \to s (suc k) \in F (s (k)))\} \leftrightarrow (suc k \in dom h (suc k) \to h (suc k) (suc k) \in F (h (suc k) (k)))$
338	328 337	imbitrdi	$⊢ ran h \subseteq S \to (h (suc k) \in ran h \to (suc k \in dom h (suc k) \to h (suc k) (suc k) \in F (h (suc k) (k))))$
339	294 298 307 338	syl3c	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to h (suc k) (suc k) \in F (h (suc k) (k))$
340	209	adantr	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to Fun ⋃ ran h$
341		elssuni	$⊢ h (suc k) \in ran h \to h (suc k) \subseteq ⋃ ran h$
342	297 341	syl	$⊢ (h : ω ⟶ S \land k \in ω) \to h (suc k) \subseteq ⋃ ran h$
343	342	adantlr	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to h (suc k) \subseteq ⋃ ran h$
344		funssfv	$⊢ (Fun ⋃ ran h \land h (suc k) \subseteq ⋃ ran h \land suc k \in dom h (suc k)) \to ⋃ ran h (suc k) = h (suc k) (suc k)$
345	340 343 307 344	syl3anc	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to ⋃ ran h (suc k) = h (suc k) (suc k)$
346	215	sseld	$⊢ h : ω ⟶ S \to (h (suc k) \in ran h \to h (suc k) \in \{s \| (\emptyset \in dom s \land dom s \in ω)\})$
347	330	eleq2d	$⊢ s = h (suc k) \to (\emptyset \in dom s \leftrightarrow \emptyset \in dom h (suc k))$
348	330	eleq1d	$⊢ s = h (suc k) \to (dom s \in ω \leftrightarrow dom h (suc k) \in ω)$
349	347 348	anbi12d	$⊢ s = h (suc k) \to ((\emptyset \in dom s \land dom s \in ω) \leftrightarrow (\emptyset \in dom h (suc k) \land dom h (suc k) \in ω))$
350	329 349	elab	$⊢ h (suc k) \in \{s \| (\emptyset \in dom s \land dom s \in ω)\} \leftrightarrow (\emptyset \in dom h (suc k) \land dom h (suc k) \in ω)$
351	346 350	imbitrdi	$⊢ h : ω ⟶ S \to (h (suc k) \in ran h \to (\emptyset \in dom h (suc k) \land dom h (suc k) \in ω))$
352	351	adantr	$⊢ (h : ω ⟶ S \land k \in ω) \to (h (suc k) \in ran h \to (\emptyset \in dom h (suc k) \land dom h (suc k) \in ω))$
353	297 352	mpd	$⊢ (h : ω ⟶ S \land k \in ω) \to (\emptyset \in dom h (suc k) \land dom h (suc k) \in ω)$
354	353	simprd	$⊢ (h : ω ⟶ S \land k \in ω) \to dom h (suc k) \in ω$
355		nnord	$⊢ dom h (suc k) \in ω \to Ord dom h (suc k)$
356		ordtr	$⊢ Ord dom h (suc k) \to Tr dom h (suc k)$
357		trsuc	$⊢ (Tr dom h (suc k) \land suc k \in dom h (suc k)) \to k \in dom h (suc k)$
358	357	ex	$⊢ Tr dom h (suc k) \to (suc k \in dom h (suc k) \to k \in dom h (suc k))$
359	354 355 356 358	4syl	$⊢ (h : ω ⟶ S \land k \in ω) \to (suc k \in dom h (suc k) \to k \in dom h (suc k))$
360	359	adantlr	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to (suc k \in dom h (suc k) \to k \in dom h (suc k))$
361	307 360	mpd	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to k \in dom h (suc k)$
362		funssfv	$⊢ (Fun ⋃ ran h \land h (suc k) \subseteq ⋃ ran h \land k \in dom h (suc k)) \to ⋃ ran h (k) = h (suc k) (k)$
363	340 343 361 362	syl3anc	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to ⋃ ran h (k) = h (suc k) (k)$
364		simpl	$⊢ (⋃ ran h (suc k) = h (suc k) (suc k) \land ⋃ ran h (k) = h (suc k) (k)) \to ⋃ ran h (suc k) = h (suc k) (suc k)$
365		simpr	$⊢ (⋃ ran h (suc k) = h (suc k) (suc k) \land ⋃ ran h (k) = h (suc k) (k)) \to ⋃ ran h (k) = h (suc k) (k)$
366	365	fveq2d	$⊢ (⋃ ran h (suc k) = h (suc k) (suc k) \land ⋃ ran h (k) = h (suc k) (k)) \to F (⋃ ran h (k)) = F (h (suc k) (k))$
367	364 366	eleq12d	$⊢ (⋃ ran h (suc k) = h (suc k) (suc k) \land ⋃ ran h (k) = h (suc k) (k)) \to (⋃ ran h (suc k) \in F (⋃ ran h (k)) \leftrightarrow h (suc k) (suc k) \in F (h (suc k) (k)))$
368	345 363 367	syl2anc	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to (⋃ ran h (suc k) \in F (⋃ ran h (k)) \leftrightarrow h (suc k) (suc k) \in F (h (suc k) (k)))$
369	339 368	mpbird	$⊢ ((h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \land k \in ω) \to ⋃ ran h (suc k) \in F (⋃ ran h (k))$
370	369	ex	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to (k \in ω \to ⋃ ran h (suc k) \in F (⋃ ran h (k)))$
371	293 370	ralrimi	$⊢ (h : ω ⟶ S \land \forall k \in ω h (suc k) \in G (h (k))) \to \forall k \in ω ⋃ ran h (suc k) \in F (⋃ ran h (k))$
372		vex	$⊢ h \in V$
373	372	rnex	$⊢ ran h \in V$
374	373	uniex	$⊢ ⋃ ran h \in V$
375		feq1	$⊢ g = ⋃ ran h \to (g : ω ⟶ A \leftrightarrow ⋃ ran h : ω ⟶ A)$
376		fveq1	$⊢ g = ⋃ ran h \to g (\emptyset) = ⋃ ran h (\emptyset)$
377	376	eqeq1d	$⊢ g = ⋃ ran h \to (g (\emptyset) = C \leftrightarrow ⋃ ran h (\emptyset) = C)$
378		fveq1	$⊢ g = ⋃ ran h \to g (suc k) = ⋃ ran h (suc k)$
379		fveq1	$⊢ g = ⋃ ran h \to g (k) = ⋃ ran h (k)$
380	379	fveq2d	$⊢ g = ⋃ ran h \to F (g (k)) = F (⋃ ran h (k))$
381	378 380	eleq12d	$⊢ g = ⋃ ran h \to (g (suc k) \in F (g (k)) \leftrightarrow ⋃ ran h (suc k) \in F (⋃ ran h (k)))$
382	381	ralbidv	$⊢ g = ⋃ ran h \to (\forall k \in ω g (suc k) \in F (g (k)) \leftrightarrow \forall k \in ω ⋃ ran h (suc k) \in F (⋃ ran h (k)))$
383	375 377 382	3anbi123d	$⊢ g = ⋃ ran h \to ((g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in F (g (k))) \leftrightarrow (⋃ ran h : ω ⟶ A \land ⋃ ran h (\emptyset) = C \land \forall k \in ω ⋃ ran h (suc k) \in F (⋃ ran h (k))))$
384	374 383	spcev	$⊢ (⋃ ran h : ω ⟶ A \land ⋃ ran h (\emptyset) = C \land \forall k \in ω ⋃ ran h (suc k) \in F (⋃ ran h (k))) \to \exists g (g : ω ⟶ A \land g (\emptyset) = C \land \forall k \in ω g (suc k) \in F (g (k)))$
385	268 290 371 384	syl3anc	$⊢ (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)))$
386	385	exlimiv	$⊢ \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)))$

Metamath Proof Explorer

Theorem axdc3lem2

Proof