axcclem

	Ref	Expression
Hypotheses	axcclem.1	$⊢ A = x ∖ \{\emptyset\}$
	axcclem.2	$⊢ F = (n \in ω, y \in ⋃ A ⟼ f (n))$
	axcclem.3	$⊢ G = (w \in A ⟼ h (suc f^{-1} (w)))$
Assertion	axcclem	$⊢ x \approx ω \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$

Proof

Step	Hyp	Ref	Expression
1		axcclem.1	$⊢ A = x ∖ \{\emptyset\}$
2		axcclem.2	$⊢ F = (n \in ω, y \in ⋃ A ⟼ f (n))$
3		axcclem.3	$⊢ G = (w \in A ⟼ h (suc f^{-1} (w)))$
4		isfinite2	$⊢ A ≺ ω \to A \in Fin$
5	1	eleq1i	$⊢ A \in Fin \leftrightarrow x ∖ \{\emptyset\} \in Fin$
6		undif1	$⊢ (x ∖ \{\emptyset\}) \cup \{\emptyset\} = x \cup \{\emptyset\}$
7		snfi	$⊢ \{\emptyset\} \in Fin$
8		unfi	$⊢ (x ∖ \{\emptyset\} \in Fin \land \{\emptyset\} \in Fin) \to (x ∖ \{\emptyset\}) \cup \{\emptyset\} \in Fin$
9	7 8	mpan2	$⊢ x ∖ \{\emptyset\} \in Fin \to (x ∖ \{\emptyset\}) \cup \{\emptyset\} \in Fin$
10	6 9	eqeltrrid	$⊢ x ∖ \{\emptyset\} \in Fin \to x \cup \{\emptyset\} \in Fin$
11		ssun1	$⊢ x \subseteq x \cup \{\emptyset\}$
12		ssfi	$⊢ (x \cup \{\emptyset\} \in Fin \land x \subseteq x \cup \{\emptyset\}) \to x \in Fin$
13	10 11 12	sylancl	$⊢ x ∖ \{\emptyset\} \in Fin \to x \in Fin$
14	5 13	sylbi	$⊢ A \in Fin \to x \in Fin$
15		dcomex	$⊢ ω \in V$
16		isfiniteg	$⊢ ω \in V \to (x \in Fin \leftrightarrow x ≺ ω)$
17	15 16	ax-mp	$⊢ x \in Fin \leftrightarrow x ≺ ω$
18		sdomnen	$⊢ x ≺ ω \to \neg x \approx ω$
19	17 18	sylbi	$⊢ x \in Fin \to \neg x \approx ω$
20	4 14 19	3syl	$⊢ A ≺ ω \to \neg x \approx ω$
21	20	con2i	$⊢ x \approx ω \to \neg A ≺ ω$
22		sdomentr	$⊢ (A ≺ x \land x \approx ω) \to A ≺ ω$
23	22	expcom	$⊢ x \approx ω \to (A ≺ x \to A ≺ ω)$
24	21 23	mtod	$⊢ x \approx ω \to \neg A ≺ x$
25		vex	$⊢ x \in V$
26		difss	$⊢ x ∖ \{\emptyset\} \subseteq x$
27	1 26	eqsstri	$⊢ A \subseteq x$
28		ssdomg	$⊢ x \in V \to (A \subseteq x \to A ≼ x)$
29	25 27 28	mp2	$⊢ A ≼ x$
30	24 29	jctil	$⊢ x \approx ω \to (A ≼ x \land \neg A ≺ x)$
31		bren2	$⊢ A \approx x \leftrightarrow (A ≼ x \land \neg A ≺ x)$
32	30 31	sylibr	$⊢ x \approx ω \to A \approx x$
33		entr	$⊢ (A \approx x \land x \approx ω) \to A \approx ω$
34	32 33	mpancom	$⊢ x \approx ω \to A \approx ω$
35		ensym	$⊢ A \approx ω \to ω \approx A$
36		bren	$⊢ ω \approx A \leftrightarrow \exists f f : ω \underset{1-1 onto}{⟶} A$
37		f1of	$⊢ f : ω \underset{1-1 onto}{⟶} A \to f : ω ⟶ A$
38		peano1	$⊢ \emptyset \in ω$
39		ffvelcdm	$⊢ (f : ω ⟶ A \land \emptyset \in ω) \to f (\emptyset) \in A$
40	37 38 39	sylancl	$⊢ f : ω \underset{1-1 onto}{⟶} A \to f (\emptyset) \in A$
41		eldifn	$⊢ f (\emptyset) \in (x ∖ \{\emptyset\}) \to \neg f (\emptyset) \in \{\emptyset\}$
42	41 1	eleq2s	$⊢ f (\emptyset) \in A \to \neg f (\emptyset) \in \{\emptyset\}$
43		fvex	$⊢ f (\emptyset) \in V$
44	43	elsn	$⊢ f (\emptyset) \in \{\emptyset\} \leftrightarrow f (\emptyset) = \emptyset$
45	44	notbii	$⊢ \neg f (\emptyset) \in \{\emptyset\} \leftrightarrow \neg f (\emptyset) = \emptyset$
46		neq0	$⊢ \neg f (\emptyset) = \emptyset \leftrightarrow \exists c c \in f (\emptyset)$
47	45 46	bitr2i	$⊢ \exists c c \in f (\emptyset) \leftrightarrow \neg f (\emptyset) \in \{\emptyset\}$
48	42 47	sylibr	$⊢ f (\emptyset) \in A \to \exists c c \in f (\emptyset)$
49	40 48	syl	$⊢ f : ω \underset{1-1 onto}{⟶} A \to \exists c c \in f (\emptyset)$
50		elunii	$⊢ (c \in f (\emptyset) \land f (\emptyset) \in A) \to c \in ⋃ A$
51	40 50	sylan2	$⊢ (c \in f (\emptyset) \land f : ω \underset{1-1 onto}{⟶} A) \to c \in ⋃ A$
52	37	ffvelcdmda	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land n \in ω) \to f (n) \in A$
53		difabs	$⊢ (x ∖ \{\emptyset\}) ∖ \{\emptyset\} = x ∖ \{\emptyset\}$
54	1	difeq1i	$⊢ A ∖ \{\emptyset\} = (x ∖ \{\emptyset\}) ∖ \{\emptyset\}$
55	53 54 1	3eqtr4i	$⊢ A ∖ \{\emptyset\} = A$
56		pwuni	$⊢ A \subseteq 𝒫 ⋃ A$
57		ssdif	$⊢ A \subseteq 𝒫 ⋃ A \to A ∖ \{\emptyset\} \subseteq 𝒫 ⋃ A ∖ \{\emptyset\}$
58	56 57	ax-mp	$⊢ A ∖ \{\emptyset\} \subseteq 𝒫 ⋃ A ∖ \{\emptyset\}$
59	55 58	eqsstrri	$⊢ A \subseteq 𝒫 ⋃ A ∖ \{\emptyset\}$
60	59	sseli	$⊢ f (n) \in A \to f (n) \in (𝒫 ⋃ A ∖ \{\emptyset\})$
61	60	ralrimivw	$⊢ f (n) \in A \to \forall y \in ⋃ A f (n) \in (𝒫 ⋃ A ∖ \{\emptyset\})$
62	52 61	syl	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land n \in ω) \to \forall y \in ⋃ A f (n) \in (𝒫 ⋃ A ∖ \{\emptyset\})$
63	62	ralrimiva	$⊢ f : ω \underset{1-1 onto}{⟶} A \to \forall n \in ω \forall y \in ⋃ A f (n) \in (𝒫 ⋃ A ∖ \{\emptyset\})$
64	2	fmpo	$⊢ \forall n \in ω \forall y \in ⋃ A f (n) \in (𝒫 ⋃ A ∖ \{\emptyset\}) \leftrightarrow F : ω \times ⋃ A ⟶ 𝒫 ⋃ A ∖ \{\emptyset\}$
65	63 64	sylib	$⊢ f : ω \underset{1-1 onto}{⟶} A \to F : ω \times ⋃ A ⟶ 𝒫 ⋃ A ∖ \{\emptyset\}$
66	65	adantl	$⊢ (c \in f (\emptyset) \land f : ω \underset{1-1 onto}{⟶} A) \to F : ω \times ⋃ A ⟶ 𝒫 ⋃ A ∖ \{\emptyset\}$
67	25	difexi	$⊢ x ∖ \{\emptyset\} \in V$
68	1 67	eqeltri	$⊢ A \in V$
69	68	uniex	$⊢ ⋃ A \in V$
70	69	axdc4	$⊢ (c \in ⋃ A \land F : ω \times ⋃ A ⟶ 𝒫 ⋃ A ∖ \{\emptyset\}) \to \exists h (h : ω ⟶ ⋃ A \land h (\emptyset) = c \land \forall k \in ω h (suc k) \in (k F h (k)))$
71	51 66 70	syl2anc	$⊢ (c \in f (\emptyset) \land f : ω \underset{1-1 onto}{⟶} A) \to \exists h (h : ω ⟶ ⋃ A \land h (\emptyset) = c \land \forall k \in ω h (suc k) \in (k F h (k)))$
72		3simpb	$⊢ (h : ω ⟶ ⋃ A \land h (\emptyset) = c \land \forall k \in ω h (suc k) \in (k F h (k))) \to (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))$
73	72	eximi	$⊢ \exists h (h : ω ⟶ ⋃ A \land h (\emptyset) = c \land \forall k \in ω h (suc k) \in (k F h (k))) \to \exists h (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))$
74	71 73	syl	$⊢ (c \in f (\emptyset) \land f : ω \underset{1-1 onto}{⟶} A) \to \exists h (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))$
75	74	ex	$⊢ c \in f (\emptyset) \to (f : ω \underset{1-1 onto}{⟶} A \to \exists h (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k))))$
76	75	exlimiv	$⊢ \exists c c \in f (\emptyset) \to (f : ω \underset{1-1 onto}{⟶} A \to \exists h (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k))))$
77	49 76	mpcom	$⊢ f : ω \underset{1-1 onto}{⟶} A \to \exists h (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))$
78		velsn	$⊢ z \in \{\emptyset\} \leftrightarrow z = \emptyset$
79	78	necon3bbii	$⊢ \neg z \in \{\emptyset\} \leftrightarrow z \neq \emptyset$
80	1	eleq2i	$⊢ z \in A \leftrightarrow z \in (x ∖ \{\emptyset\})$
81		eldif	$⊢ z \in (x ∖ \{\emptyset\}) \leftrightarrow (z \in x \land \neg z \in \{\emptyset\})$
82	80 81	sylbbr	$⊢ (z \in x \land \neg z \in \{\emptyset\}) \to z \in A$
83	79 82	sylan2br	$⊢ (z \in x \land z \neq \emptyset) \to z \in A$
84		simpl	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land z \in A) \to f : ω \underset{1-1 onto}{⟶} A$
85		f1ofo	$⊢ f : ω \underset{1-1 onto}{⟶} A \to f : ω \underset{onto}{⟶} A$
86		foelrn	$⊢ (f : ω \underset{onto}{⟶} A \land z \in A) \to \exists i \in ω z = f (i)$
87	85 86	sylan	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land z \in A) \to \exists i \in ω z = f (i)$
88		suceq	$⊢ k = i \to suc k = suc i$
89	88	fveq2d	$⊢ k = i \to h (suc k) = h (suc i)$
90		id	$⊢ k = i \to k = i$
91		fveq2	$⊢ k = i \to h (k) = h (i)$
92	90 91	oveq12d	$⊢ k = i \to k F h (k) = i F h (i)$
93	89 92	eleq12d	$⊢ k = i \to (h (suc k) \in (k F h (k)) \leftrightarrow h (suc i) \in (i F h (i)))$
94	93	rspcv	$⊢ i \in ω \to (\forall k \in ω h (suc k) \in (k F h (k)) \to h (suc i) \in (i F h (i)))$
95	94	3ad2ant3	$⊢ (h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to (\forall k \in ω h (suc k) \in (k F h (k)) \to h (suc i) \in (i F h (i)))$
96	95	imp	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k))) \to h (suc i) \in (i F h (i))$
97	96	3adant3	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to h (suc i) \in (i F h (i))$
98		eqcom	$⊢ z = f (i) \leftrightarrow f (i) = z$
99		f1ocnvfv	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to (f (i) = z \to f^{-1} (z) = i)$
100	98 99	biimtrid	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to (z = f (i) \to f^{-1} (z) = i)$
101	100	3adant1	$⊢ (h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to (z = f (i) \to f^{-1} (z) = i)$
102	101	imp	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land z = f (i)) \to f^{-1} (z) = i$
103	102	eqcomd	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land z = f (i)) \to i = f^{-1} (z)$
104	103	3adant2	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to i = f^{-1} (z)$
105		suceq	$⊢ i = f^{-1} (z) \to suc i = suc f^{-1} (z)$
106	104 105	syl	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to suc i = suc f^{-1} (z)$
107	106	fveq2d	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to h (suc i) = h (suc f^{-1} (z))$
108		simpr	$⊢ (h : ω ⟶ ⋃ A \land i \in ω) \to i \in ω$
109		ffvelcdm	$⊢ (h : ω ⟶ ⋃ A \land i \in ω) \to h (i) \in ⋃ A$
110		fveq2	$⊢ n = i \to f (n) = f (i)$
111		eqidd	$⊢ y = h (i) \to f (i) = f (i)$
112		fvex	$⊢ f (i) \in V$
113	110 111 2 112	ovmpo	$⊢ (i \in ω \land h (i) \in ⋃ A) \to i F h (i) = f (i)$
114	108 109 113	syl2anc	$⊢ (h : ω ⟶ ⋃ A \land i \in ω) \to i F h (i) = f (i)$
115	114	3adant2	$⊢ (h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to i F h (i) = f (i)$
116	115	3ad2ant1	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to i F h (i) = f (i)$
117	97 107 116	3eltr3d	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to h (suc f^{-1} (z)) \in f (i)$
118	37	ffvelcdmda	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to f (i) \in A$
119	118	3adant1	$⊢ (h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to f (i) \in A$
120	119	3ad2ant1	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to f (i) \in A$
121		eleq1	$⊢ z = f (i) \to (z \in A \leftrightarrow f (i) \in A)$
122	121	3ad2ant3	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to (z \in A \leftrightarrow f (i) \in A)$
123	120 122	mpbird	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to z \in A$
124		fveq2	$⊢ w = z \to f^{-1} (w) = f^{-1} (z)$
125		suceq	$⊢ f^{-1} (w) = f^{-1} (z) \to suc f^{-1} (w) = suc f^{-1} (z)$
126	124 125	syl	$⊢ w = z \to suc f^{-1} (w) = suc f^{-1} (z)$
127	126	fveq2d	$⊢ w = z \to h (suc f^{-1} (w)) = h (suc f^{-1} (z))$
128		fvex	$⊢ h (suc f^{-1} (z)) \in V$
129	127 3 128	fvmpt	$⊢ z \in A \to G (z) = h (suc f^{-1} (z))$
130	123 129	syl	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to G (z) = h (suc f^{-1} (z))$
131		simp3	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to z = f (i)$
132	117 130 131	3eltr4d	$⊢ ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \land \forall k \in ω h (suc k) \in (k F h (k)) \land z = f (i)) \to G (z) \in z$
133	132	3exp	$⊢ (h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to (\forall k \in ω h (suc k) \in (k F h (k)) \to (z = f (i) \to G (z) \in z))$
134	133	com3r	$⊢ z = f (i) \to ((h : ω ⟶ ⋃ A \land f : ω \underset{1-1 onto}{⟶} A \land i \in ω) \to (\forall k \in ω h (suc k) \in (k F h (k)) \to G (z) \in z))$
135	134	3expd	$⊢ z = f (i) \to (h : ω ⟶ ⋃ A \to (f : ω \underset{1-1 onto}{⟶} A \to (i \in ω \to (\forall k \in ω h (suc k) \in (k F h (k)) \to G (z) \in z))))$
136	135	com4r	$⊢ i \in ω \to (z = f (i) \to (h : ω ⟶ ⋃ A \to (f : ω \underset{1-1 onto}{⟶} A \to (\forall k \in ω h (suc k) \in (k F h (k)) \to G (z) \in z))))$
137	136	rexlimiv	$⊢ \exists i \in ω z = f (i) \to (h : ω ⟶ ⋃ A \to (f : ω \underset{1-1 onto}{⟶} A \to (\forall k \in ω h (suc k) \in (k F h (k)) \to G (z) \in z)))$
138	87 137	syl	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land z \in A) \to (h : ω ⟶ ⋃ A \to (f : ω \underset{1-1 onto}{⟶} A \to (\forall k \in ω h (suc k) \in (k F h (k)) \to G (z) \in z)))$
139	84 138	mpid	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land z \in A) \to (h : ω ⟶ ⋃ A \to (\forall k \in ω h (suc k) \in (k F h (k)) \to G (z) \in z))$
140	139	impd	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land z \in A) \to ((h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k))) \to G (z) \in z)$
141	140	impancom	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))) \to (z \in A \to G (z) \in z)$
142	83 141	syl5	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))) \to ((z \in x \land z \neq \emptyset) \to G (z) \in z)$
143	142	expd	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))) \to (z \in x \to (z \neq \emptyset \to G (z) \in z))$
144	143	ralrimiv	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))) \to \forall z \in x (z \neq \emptyset \to G (z) \in z)$
145		fvrn0	$⊢ h (suc f^{-1} (w)) \in (ran h \cup \{\emptyset\})$
146	145	rgenw	$⊢ \forall w \in A h (suc f^{-1} (w)) \in (ran h \cup \{\emptyset\})$
147		eqid	$⊢ (w \in A ⟼ h (suc f^{-1} (w))) = (w \in A ⟼ h (suc f^{-1} (w)))$
148	147	fmpt	$⊢ \forall w \in A h (suc f^{-1} (w)) \in (ran h \cup \{\emptyset\}) \leftrightarrow (w \in A ⟼ h (suc f^{-1} (w))) : A ⟶ ran h \cup \{\emptyset\}$
149	146 148	mpbi	$⊢ (w \in A ⟼ h (suc f^{-1} (w))) : A ⟶ ran h \cup \{\emptyset\}$
150		vex	$⊢ h \in V$
151	150	rnex	$⊢ ran h \in V$
152		p0ex	$⊢ \{\emptyset\} \in V$
153	151 152	unex	$⊢ ran h \cup \{\emptyset\} \in V$
154		fex2	$⊢ ((w \in A ⟼ h (suc f^{-1} (w))) : A ⟶ ran h \cup \{\emptyset\} \land A \in V \land ran h \cup \{\emptyset\} \in V) \to (w \in A ⟼ h (suc f^{-1} (w))) \in V$
155	149 68 153 154	mp3an	$⊢ (w \in A ⟼ h (suc f^{-1} (w))) \in V$
156	3 155	eqeltri	$⊢ G \in V$
157		fveq1	$⊢ g = G \to g (z) = G (z)$
158	157	eleq1d	$⊢ g = G \to (g (z) \in z \leftrightarrow G (z) \in z)$
159	158	imbi2d	$⊢ g = G \to ((z \neq \emptyset \to g (z) \in z) \leftrightarrow (z \neq \emptyset \to G (z) \in z))$
160	159	ralbidv	$⊢ g = G \to (\forall z \in x (z \neq \emptyset \to g (z) \in z) \leftrightarrow \forall z \in x (z \neq \emptyset \to G (z) \in z))$
161	156 160	spcev	$⊢ \forall z \in x (z \neq \emptyset \to G (z) \in z) \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$
162	144 161	syl	$⊢ (f : ω \underset{1-1 onto}{⟶} A \land (h : ω ⟶ ⋃ A \land \forall k \in ω h (suc k) \in (k F h (k)))) \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$
163	77 162	exlimddv	$⊢ f : ω \underset{1-1 onto}{⟶} A \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$
164	163	exlimiv	$⊢ \exists f f : ω \underset{1-1 onto}{⟶} A \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$
165	36 164	sylbi	$⊢ ω \approx A \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$
166	34 35 165	3syl	$⊢ x \approx ω \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$

Metamath Proof Explorer

Theorem axcclem

Proof