axcc3

Description: A possibly more useful version of ax-cc using sequences F ( n ) instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013) (Revised by Mario Carneiro, 26-Dec-2014)

	Ref	Expression
Hypotheses	axcc3.1	$⊢ F \in V$
	axcc3.2	$⊢ N \approx ω$
Assertion	axcc3	$⊢ \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F))$

Proof

Step	Hyp	Ref	Expression
1		axcc3.1	$⊢ F \in V$
2		axcc3.2	$⊢ N \approx ω$
3		relen	$⊢ Rel \approx$
4	3	brrelex1i	$⊢ N \approx ω \to N \in V$
5		mptexg	$⊢ N \in V \to (n \in N ⟼ F) \in V$
6	2 4 5	mp2b	$⊢ (n \in N ⟼ F) \in V$
7		bren	$⊢ N \approx ω \leftrightarrow \exists h h : N \underset{1-1 onto}{⟶} ω$
8	2 7	mpbi	$⊢ \exists h h : N \underset{1-1 onto}{⟶} ω$
9		axcc2	$⊢ \exists g (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)))$
10		f1of	$⊢ h : N \underset{1-1 onto}{⟶} ω \to h : N ⟶ ω$
11		fnfco	$⊢ (g Fn ω \land h : N ⟶ ω) \to (g \circ h) Fn N$
12	10 11	sylan2	$⊢ (g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \to (g \circ h) Fn N$
13	12	adantlr	$⊢ ((g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \land h : N \underset{1-1 onto}{⟶} ω) \to (g \circ h) Fn N$
14	13	3adant1	$⊢ (k = (n \in N ⟼ F) \land (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \land h : N \underset{1-1 onto}{⟶} ω) \to (g \circ h) Fn N$
15		nfmpt1	$⊢ \underline{Ⅎ} n (n \in N ⟼ F)$
16	15	nfeq2	$⊢ Ⅎ n k = (n \in N ⟼ F)$
17		nfv	$⊢ Ⅎ n (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)))$
18		nfv	$⊢ Ⅎ n h : N \underset{1-1 onto}{⟶} ω$
19	16 17 18	nf3an	$⊢ Ⅎ n (k = (n \in N ⟼ F) \land (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \land h : N \underset{1-1 onto}{⟶} ω)$
20	10	ffvelcdmda	$⊢ (h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to h (n) \in ω$
21		fveq2	$⊢ m = h (n) \to (k \circ h^{-1}) (m) = (k \circ h^{-1}) (h (n))$
22	21	neeq1d	$⊢ m = h (n) \to ((k \circ h^{-1}) (m) \neq \emptyset \leftrightarrow (k \circ h^{-1}) (h (n)) \neq \emptyset)$
23		fveq2	$⊢ m = h (n) \to g (m) = g (h (n))$
24	23 21	eleq12d	$⊢ m = h (n) \to (g (m) \in (k \circ h^{-1}) (m) \leftrightarrow g (h (n)) \in (k \circ h^{-1}) (h (n)))$
25	22 24	imbi12d	$⊢ m = h (n) \to (((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \leftrightarrow ((k \circ h^{-1}) (h (n)) \neq \emptyset \to g (h (n)) \in (k \circ h^{-1}) (h (n))))$
26	25	rspcv	$⊢ h (n) \in ω \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to ((k \circ h^{-1}) (h (n)) \neq \emptyset \to g (h (n)) \in (k \circ h^{-1}) (h (n))))$
27	20 26	syl	$⊢ (h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to ((k \circ h^{-1}) (h (n)) \neq \emptyset \to g (h (n)) \in (k \circ h^{-1}) (h (n))))$
28	27	3ad2antl3	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to ((k \circ h^{-1}) (h (n)) \neq \emptyset \to g (h (n)) \in (k \circ h^{-1}) (h (n))))$
29		f1ocnv	$⊢ h : N \underset{1-1 onto}{⟶} ω \to h^{-1} : ω \underset{1-1 onto}{⟶} N$
30		f1of	$⊢ h^{-1} : ω \underset{1-1 onto}{⟶} N \to h^{-1} : ω ⟶ N$
31	29 30	syl	$⊢ h : N \underset{1-1 onto}{⟶} ω \to h^{-1} : ω ⟶ N$
32		fvco3	$⊢ (h^{-1} : ω ⟶ N \land h (n) \in ω) \to (k \circ h^{-1}) (h (n)) = k (h^{-1} (h (n)))$
33	31 20 32	syl2an2r	$⊢ (h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to (k \circ h^{-1}) (h (n)) = k (h^{-1} (h (n)))$
34	33	3adant1	$⊢ (k = (n \in N ⟼ F) \land h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to (k \circ h^{-1}) (h (n)) = k (h^{-1} (h (n)))$
35		f1ocnvfv1	$⊢ (h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to h^{-1} (h (n)) = n$
36	35	fveq2d	$⊢ (h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to k (h^{-1} (h (n))) = k (n)$
37	36	3adant1	$⊢ (k = (n \in N ⟼ F) \land h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to k (h^{-1} (h (n))) = k (n)$
38		fveq1	$⊢ k = (n \in N ⟼ F) \to k (n) = (n \in N ⟼ F) (n)$
39		eqid	$⊢ (n \in N ⟼ F) = (n \in N ⟼ F)$
40	39	fvmpt2	$⊢ (n \in N \land F \in V) \to (n \in N ⟼ F) (n) = F$
41	1 40	mpan2	$⊢ n \in N \to (n \in N ⟼ F) (n) = F$
42	38 41	sylan9eq	$⊢ (k = (n \in N ⟼ F) \land n \in N) \to k (n) = F$
43	42	3adant2	$⊢ (k = (n \in N ⟼ F) \land h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to k (n) = F$
44	34 37 43	3eqtrd	$⊢ (k = (n \in N ⟼ F) \land h : N \underset{1-1 onto}{⟶} ω \land n \in N) \to (k \circ h^{-1}) (h (n)) = F$
45	44	3expa	$⊢ ((k = (n \in N ⟼ F) \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to (k \circ h^{-1}) (h (n)) = F$
46	45	3adantl2	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to (k \circ h^{-1}) (h (n)) = F$
47	46	neeq1d	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to ((k \circ h^{-1}) (h (n)) \neq \emptyset \leftrightarrow F \neq \emptyset)$
48	10	3ad2ant3	$⊢ (k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \to h : N ⟶ ω$
49		fvco3	$⊢ (h : N ⟶ ω \land n \in N) \to (g \circ h) (n) = g (h (n))$
50	48 49	sylan	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to (g \circ h) (n) = g (h (n))$
51	50	eleq1d	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to ((g \circ h) (n) \in (k \circ h^{-1}) (h (n)) \leftrightarrow g (h (n)) \in (k \circ h^{-1}) (h (n)))$
52	46	eleq2d	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to ((g \circ h) (n) \in (k \circ h^{-1}) (h (n)) \leftrightarrow (g \circ h) (n) \in F)$
53	51 52	bitr3d	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to (g (h (n)) \in (k \circ h^{-1}) (h (n)) \leftrightarrow (g \circ h) (n) \in F)$
54	47 53	imbi12d	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to (((k \circ h^{-1}) (h (n)) \neq \emptyset \to g (h (n)) \in (k \circ h^{-1}) (h (n))) \leftrightarrow (F \neq \emptyset \to (g \circ h) (n) \in F))$
55	28 54	sylibd	$⊢ ((k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \land n \in N) \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to (F \neq \emptyset \to (g \circ h) (n) \in F))$
56	55	ex	$⊢ (k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \to (n \in N \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to (F \neq \emptyset \to (g \circ h) (n) \in F)))$
57	56	com23	$⊢ (k = (n \in N ⟼ F) \land g Fn ω \land h : N \underset{1-1 onto}{⟶} ω) \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to (n \in N \to (F \neq \emptyset \to (g \circ h) (n) \in F)))$
58	57	3exp	$⊢ k = (n \in N ⟼ F) \to (g Fn ω \to (h : N \underset{1-1 onto}{⟶} ω \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to (n \in N \to (F \neq \emptyset \to (g \circ h) (n) \in F)))))$
59	58	com34	$⊢ k = (n \in N ⟼ F) \to (g Fn ω \to (\forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)) \to (h : N \underset{1-1 onto}{⟶} ω \to (n \in N \to (F \neq \emptyset \to (g \circ h) (n) \in F)))))$
60	59	imp32	$⊢ (k = (n \in N ⟼ F) \land (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m)))) \to (h : N \underset{1-1 onto}{⟶} ω \to (n \in N \to (F \neq \emptyset \to (g \circ h) (n) \in F)))$
61	60	3impia	$⊢ (k = (n \in N ⟼ F) \land (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \land h : N \underset{1-1 onto}{⟶} ω) \to (n \in N \to (F \neq \emptyset \to (g \circ h) (n) \in F))$
62	19 61	ralrimi	$⊢ (k = (n \in N ⟼ F) \land (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \land h : N \underset{1-1 onto}{⟶} ω) \to \forall n \in N (F \neq \emptyset \to (g \circ h) (n) \in F)$
63		vex	$⊢ g \in V$
64		vex	$⊢ h \in V$
65	63 64	coex	$⊢ g \circ h \in V$
66		fneq1	$⊢ f = g \circ h \to (f Fn N \leftrightarrow (g \circ h) Fn N)$
67		fveq1	$⊢ f = g \circ h \to f (n) = (g \circ h) (n)$
68	67	eleq1d	$⊢ f = g \circ h \to (f (n) \in F \leftrightarrow (g \circ h) (n) \in F)$
69	68	imbi2d	$⊢ f = g \circ h \to ((F \neq \emptyset \to f (n) \in F) \leftrightarrow (F \neq \emptyset \to (g \circ h) (n) \in F))$
70	69	ralbidv	$⊢ f = g \circ h \to (\forall n \in N (F \neq \emptyset \to f (n) \in F) \leftrightarrow \forall n \in N (F \neq \emptyset \to (g \circ h) (n) \in F))$
71	66 70	anbi12d	$⊢ f = g \circ h \to ((f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F)) \leftrightarrow ((g \circ h) Fn N \land \forall n \in N (F \neq \emptyset \to (g \circ h) (n) \in F)))$
72	65 71	spcev	$⊢ ((g \circ h) Fn N \land \forall n \in N (F \neq \emptyset \to (g \circ h) (n) \in F)) \to \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F))$
73	14 62 72	syl2anc	$⊢ (k = (n \in N ⟼ F) \land (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \land h : N \underset{1-1 onto}{⟶} ω) \to \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F))$
74	73	3exp	$⊢ k = (n \in N ⟼ F) \to ((g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \to (h : N \underset{1-1 onto}{⟶} ω \to \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F))))$
75	74	exlimdv	$⊢ k = (n \in N ⟼ F) \to (\exists g (g Fn ω \land \forall m \in ω ((k \circ h^{-1}) (m) \neq \emptyset \to g (m) \in (k \circ h^{-1}) (m))) \to (h : N \underset{1-1 onto}{⟶} ω \to \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F))))$
76	9 75	mpi	$⊢ k = (n \in N ⟼ F) \to (h : N \underset{1-1 onto}{⟶} ω \to \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F)))$
77	76	exlimdv	$⊢ k = (n \in N ⟼ F) \to (\exists h h : N \underset{1-1 onto}{⟶} ω \to \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F)))$
78	8 77	mpi	$⊢ k = (n \in N ⟼ F) \to \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F))$
79	6 78	vtocle	$⊢ \exists f (f Fn N \land \forall n \in N (F \neq \emptyset \to f (n) \in F))$

Metamath Proof Explorer

Theorem axcc3

Proof