axcc2lem

	Ref	Expression
Hypotheses	axcc2lem.1	$⊢ K = (n \in ω ⟼ if (F (n) = \emptyset, \{\emptyset\}, F (n)))$
	axcc2lem.2	$⊢ A = (n \in ω ⟼ \{n\} \times K (n))$
	axcc2lem.3	$⊢ G = (n \in ω ⟼ 2^{nd} (f (A (n))))$
Assertion	axcc2lem	$⊢ \exists g (g Fn ω \land \forall n \in ω (F (n) \neq \emptyset \to g (n) \in F (n)))$

Proof

Step	Hyp	Ref	Expression
1		axcc2lem.1	$⊢ K = (n \in ω ⟼ if (F (n) = \emptyset, \{\emptyset\}, F (n)))$
2		axcc2lem.2	$⊢ A = (n \in ω ⟼ \{n\} \times K (n))$
3		axcc2lem.3	$⊢ G = (n \in ω ⟼ 2^{nd} (f (A (n))))$
4		fvex	$⊢ 2^{nd} (f (A (n))) \in V$
5	4 3	fnmpti	$⊢ G Fn ω$
6		snex	$⊢ \{n\} \in V$
7		fvex	$⊢ K (n) \in V$
8	6 7	xpex	$⊢ \{n\} \times K (n) \in V$
9	2	fvmpt2	$⊢ (n \in ω \land \{n\} \times K (n) \in V) \to A (n) = \{n\} \times K (n)$
10	8 9	mpan2	$⊢ n \in ω \to A (n) = \{n\} \times K (n)$
11		vex	$⊢ n \in V$
12	11	snnz	$⊢ \{n\} \neq \emptyset$
13		0ex	$⊢ \emptyset \in V$
14	13	snnz	$⊢ \{\emptyset\} \neq \emptyset$
15		iftrue	$⊢ F (n) = \emptyset \to if (F (n) = \emptyset, \{\emptyset\}, F (n)) = \{\emptyset\}$
16	15	neeq1d	$⊢ F (n) = \emptyset \to (if (F (n) = \emptyset, \{\emptyset\}, F (n)) \neq \emptyset \leftrightarrow \{\emptyset\} \neq \emptyset)$
17	14 16	mpbiri	$⊢ F (n) = \emptyset \to if (F (n) = \emptyset, \{\emptyset\}, F (n)) \neq \emptyset$
18		iffalse	$⊢ \neg F (n) = \emptyset \to if (F (n) = \emptyset, \{\emptyset\}, F (n)) = F (n)$
19		neqne	$⊢ \neg F (n) = \emptyset \to F (n) \neq \emptyset$
20	18 19	eqnetrd	$⊢ \neg F (n) = \emptyset \to if (F (n) = \emptyset, \{\emptyset\}, F (n)) \neq \emptyset$
21	17 20	pm2.61i	$⊢ if (F (n) = \emptyset, \{\emptyset\}, F (n)) \neq \emptyset$
22		p0ex	$⊢ \{\emptyset\} \in V$
23		fvex	$⊢ F (n) \in V$
24	22 23	ifex	$⊢ if (F (n) = \emptyset, \{\emptyset\}, F (n)) \in V$
25	1	fvmpt2	$⊢ (n \in ω \land if (F (n) = \emptyset, \{\emptyset\}, F (n)) \in V) \to K (n) = if (F (n) = \emptyset, \{\emptyset\}, F (n))$
26	24 25	mpan2	$⊢ n \in ω \to K (n) = if (F (n) = \emptyset, \{\emptyset\}, F (n))$
27	26	neeq1d	$⊢ n \in ω \to (K (n) \neq \emptyset \leftrightarrow if (F (n) = \emptyset, \{\emptyset\}, F (n)) \neq \emptyset)$
28	21 27	mpbiri	$⊢ n \in ω \to K (n) \neq \emptyset$
29		xpnz	$⊢ (\{n\} \neq \emptyset \land K (n) \neq \emptyset) \leftrightarrow \{n\} \times K (n) \neq \emptyset$
30	29	biimpi	$⊢ (\{n\} \neq \emptyset \land K (n) \neq \emptyset) \to \{n\} \times K (n) \neq \emptyset$
31	12 28 30	sylancr	$⊢ n \in ω \to \{n\} \times K (n) \neq \emptyset$
32	10 31	eqnetrd	$⊢ n \in ω \to A (n) \neq \emptyset$
33	8 2	fnmpti	$⊢ A Fn ω$
34		fnfvelrn	$⊢ (A Fn ω \land n \in ω) \to A (n) \in ran A$
35	33 34	mpan	$⊢ n \in ω \to A (n) \in ran A$
36		neeq1	$⊢ z = A (n) \to (z \neq \emptyset \leftrightarrow A (n) \neq \emptyset)$
37		fveq2	$⊢ z = A (n) \to f (z) = f (A (n))$
38		id	$⊢ z = A (n) \to z = A (n)$
39	37 38	eleq12d	$⊢ z = A (n) \to (f (z) \in z \leftrightarrow f (A (n)) \in A (n))$
40	36 39	imbi12d	$⊢ z = A (n) \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (A (n) \neq \emptyset \to f (A (n)) \in A (n)))$
41	40	rspccv	$⊢ \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \to (A (n) \in ran A \to (A (n) \neq \emptyset \to f (A (n)) \in A (n)))$
42	35 41	syl5	$⊢ \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \to (n \in ω \to (A (n) \neq \emptyset \to f (A (n)) \in A (n)))$
43	32 42	mpdi	$⊢ \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \to (n \in ω \to f (A (n)) \in A (n))$
44	43	impcom	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z)) \to f (A (n)) \in A (n)$
45	10	eleq2d	$⊢ n \in ω \to (f (A (n)) \in A (n) \leftrightarrow f (A (n)) \in (\{n\} \times K (n)))$
46	45	adantr	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z)) \to (f (A (n)) \in A (n) \leftrightarrow f (A (n)) \in (\{n\} \times K (n)))$
47	44 46	mpbid	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z)) \to f (A (n)) \in (\{n\} \times K (n))$
48		xp2nd	$⊢ f (A (n)) \in (\{n\} \times K (n)) \to 2^{nd} (f (A (n))) \in K (n)$
49	47 48	syl	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z)) \to 2^{nd} (f (A (n))) \in K (n)$
50	49	3adant3	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \land F (n) \neq \emptyset) \to 2^{nd} (f (A (n))) \in K (n)$
51	3	fvmpt2	$⊢ (n \in ω \land 2^{nd} (f (A (n))) \in V) \to G (n) = 2^{nd} (f (A (n)))$
52	4 51	mpan2	$⊢ n \in ω \to G (n) = 2^{nd} (f (A (n)))$
53	52	3ad2ant1	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \land F (n) \neq \emptyset) \to G (n) = 2^{nd} (f (A (n)))$
54	53	eqcomd	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \land F (n) \neq \emptyset) \to 2^{nd} (f (A (n))) = G (n)$
55	26	3ad2ant1	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \land F (n) \neq \emptyset) \to K (n) = if (F (n) = \emptyset, \{\emptyset\}, F (n))$
56		ifnefalse	$⊢ F (n) \neq \emptyset \to if (F (n) = \emptyset, \{\emptyset\}, F (n)) = F (n)$
57	56	3ad2ant3	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \land F (n) \neq \emptyset) \to if (F (n) = \emptyset, \{\emptyset\}, F (n)) = F (n)$
58	55 57	eqtrd	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \land F (n) \neq \emptyset) \to K (n) = F (n)$
59	50 54 58	3eltr3d	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \land F (n) \neq \emptyset) \to G (n) \in F (n)$
60	59	3expia	$⊢ (n \in ω \land \forall z \in ran A (z \neq \emptyset \to f (z) \in z)) \to (F (n) \neq \emptyset \to G (n) \in F (n))$
61	60	expcom	$⊢ \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \to (n \in ω \to (F (n) \neq \emptyset \to G (n) \in F (n)))$
62	61	ralrimiv	$⊢ \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \to \forall n \in ω (F (n) \neq \emptyset \to G (n) \in F (n))$
63		omex	$⊢ ω \in V$
64		fnex	$⊢ (G Fn ω \land ω \in V) \to G \in V$
65	5 63 64	mp2an	$⊢ G \in V$
66		fneq1	$⊢ g = G \to (g Fn ω \leftrightarrow G Fn ω)$
67		fveq1	$⊢ g = G \to g (n) = G (n)$
68	67	eleq1d	$⊢ g = G \to (g (n) \in F (n) \leftrightarrow G (n) \in F (n))$
69	68	imbi2d	$⊢ g = G \to ((F (n) \neq \emptyset \to g (n) \in F (n)) \leftrightarrow (F (n) \neq \emptyset \to G (n) \in F (n)))$
70	69	ralbidv	$⊢ g = G \to (\forall n \in ω (F (n) \neq \emptyset \to g (n) \in F (n)) \leftrightarrow \forall n \in ω (F (n) \neq \emptyset \to G (n) \in F (n)))$
71	66 70	anbi12d	$⊢ g = G \to ((g Fn ω \land \forall n \in ω (F (n) \neq \emptyset \to g (n) \in F (n))) \leftrightarrow (G Fn ω \land \forall n \in ω (F (n) \neq \emptyset \to G (n) \in F (n))))$
72	65 71	spcev	$⊢ (G Fn ω \land \forall n \in ω (F (n) \neq \emptyset \to G (n) \in F (n))) \to \exists g (g Fn ω \land \forall n \in ω (F (n) \neq \emptyset \to g (n) \in F (n)))$
73	5 62 72	sylancr	$⊢ \forall z \in ran A (z \neq \emptyset \to f (z) \in z) \to \exists g (g Fn ω \land \forall n \in ω (F (n) \neq \emptyset \to g (n) \in F (n)))$
74	8	a1i	$⊢ (ω \in V \land n \in ω) \to \{n\} \times K (n) \in V$
75	74 2	fmptd	$⊢ ω \in V \to A : ω ⟶ V$
76	63 75	ax-mp	$⊢ A : ω ⟶ V$
77		sneq	$⊢ n = k \to \{n\} = \{k\}$
78		fveq2	$⊢ n = k \to K (n) = K (k)$
79	77 78	xpeq12d	$⊢ n = k \to \{n\} \times K (n) = \{k\} \times K (k)$
80	79 2 8	fvmpt3i	$⊢ k \in ω \to A (k) = \{k\} \times K (k)$
81	80	adantl	$⊢ (n \in ω \land k \in ω) \to A (k) = \{k\} \times K (k)$
82	81	eqeq2d	$⊢ (n \in ω \land k \in ω) \to (A (n) = A (k) \leftrightarrow A (n) = \{k\} \times K (k))$
83	10	adantr	$⊢ (n \in ω \land k \in ω) \to A (n) = \{n\} \times K (n)$
84	83	eqeq1d	$⊢ (n \in ω \land k \in ω) \to (A (n) = \{k\} \times K (k) \leftrightarrow \{n\} \times K (n) = \{k\} \times K (k))$
85		xp11	$⊢ (\{n\} \neq \emptyset \land K (n) \neq \emptyset) \to (\{n\} \times K (n) = \{k\} \times K (k) \leftrightarrow (\{n\} = \{k\} \land K (n) = K (k)))$
86	12 28 85	sylancr	$⊢ n \in ω \to (\{n\} \times K (n) = \{k\} \times K (k) \leftrightarrow (\{n\} = \{k\} \land K (n) = K (k)))$
87	11	sneqr	$⊢ \{n\} = \{k\} \to n = k$
88	87	adantr	$⊢ (\{n\} = \{k\} \land K (n) = K (k)) \to n = k$
89	86 88	syl6bi	$⊢ n \in ω \to (\{n\} \times K (n) = \{k\} \times K (k) \to n = k)$
90	89	adantr	$⊢ (n \in ω \land k \in ω) \to (\{n\} \times K (n) = \{k\} \times K (k) \to n = k)$
91	84 90	sylbid	$⊢ (n \in ω \land k \in ω) \to (A (n) = \{k\} \times K (k) \to n = k)$
92	82 91	sylbid	$⊢ (n \in ω \land k \in ω) \to (A (n) = A (k) \to n = k)$
93	92	rgen2	$⊢ \forall n \in ω \forall k \in ω (A (n) = A (k) \to n = k)$
94		dff13	$⊢ A : ω \underset{1-1}{⟶} V \leftrightarrow (A : ω ⟶ V \land \forall n \in ω \forall k \in ω (A (n) = A (k) \to n = k))$
95	76 93 94	mpbir2an	$⊢ A : ω \underset{1-1}{⟶} V$
96		f1f1orn	$⊢ A : ω \underset{1-1}{⟶} V \to A : ω \underset{1-1 onto}{⟶} ran A$
97	63	f1oen	$⊢ A : ω \underset{1-1 onto}{⟶} ran A \to ω \approx ran A$
98		ensym	$⊢ ω \approx ran A \to ran A \approx ω$
99	96 97 98	3syl	$⊢ A : ω \underset{1-1}{⟶} V \to ran A \approx ω$
100	2	rneqi	$⊢ ran A = ran (n \in ω ⟼ \{n\} \times K (n))$
101		dmmptg	$⊢ \forall n \in ω \{n\} \times K (n) \in V \to dom (n \in ω ⟼ \{n\} \times K (n)) = ω$
102	8	a1i	$⊢ n \in ω \to \{n\} \times K (n) \in V$
103	101 102	mprg	$⊢ dom (n \in ω ⟼ \{n\} \times K (n)) = ω$
104	103 63	eqeltri	$⊢ dom (n \in ω ⟼ \{n\} \times K (n)) \in V$
105		funmpt	$⊢ Fun (n \in ω ⟼ \{n\} \times K (n))$
106		funrnex	$⊢ dom (n \in ω ⟼ \{n\} \times K (n)) \in V \to (Fun (n \in ω ⟼ \{n\} \times K (n)) \to ran (n \in ω ⟼ \{n\} \times K (n)) \in V)$
107	104 105 106	mp2	$⊢ ran (n \in ω ⟼ \{n\} \times K (n)) \in V$
108	100 107	eqeltri	$⊢ ran A \in V$
109		breq1	$⊢ a = ran A \to (a \approx ω \leftrightarrow ran A \approx ω)$
110		raleq	$⊢ a = ran A \to (\forall z \in a (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall z \in ran A (z \neq \emptyset \to f (z) \in z))$
111	110	exbidv	$⊢ a = ran A \to (\exists f \forall z \in a (z \neq \emptyset \to f (z) \in z) \leftrightarrow \exists f \forall z \in ran A (z \neq \emptyset \to f (z) \in z))$
112	109 111	imbi12d	$⊢ a = ran A \to ((a \approx ω \to \exists f \forall z \in a (z \neq \emptyset \to f (z) \in z)) \leftrightarrow (ran A \approx ω \to \exists f \forall z \in ran A (z \neq \emptyset \to f (z) \in z)))$
113		ax-cc	$⊢ a \approx ω \to \exists f \forall z \in a (z \neq \emptyset \to f (z) \in z)$
114	108 112 113	vtocl	$⊢ ran A \approx ω \to \exists f \forall z \in ran A (z \neq \emptyset \to f (z) \in z)$
115	95 99 114	mp2b	$⊢ \exists f \forall z \in ran A (z \neq \emptyset \to f (z) \in z)$
116	73 115	exlimiiv	$⊢ \exists g (g Fn ω \land \forall n \in ω (F (n) \neq \emptyset \to g (n) \in F (n)))$

Metamath Proof Explorer

Theorem axcc2lem

Proof