axccdom

Description: Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	axccdom.1	$⊢ φ \to X ≼ ω$
	axccdom.2	$⊢ (φ \land z \in X) \to z \neq \emptyset$
Assertion	axccdom	$⊢ φ \to \exists f (f Fn X \land \forall z \in X f (z) \in z)$

Proof

Step	Hyp	Ref	Expression
1		axccdom.1	$⊢ φ \to X ≼ ω$
2		axccdom.2	$⊢ (φ \land z \in X) \to z \neq \emptyset$
3		simpr	$⊢ (φ \land X \in Fin) \to X \in Fin$
4		simpr	$⊢ ((φ \land X \in Fin) \land z \in X) \to z \in X$
5	2	adantlr	$⊢ ((φ \land X \in Fin) \land z \in X) \to z \neq \emptyset$
6	3 4 5	choicefi	$⊢ (φ \land X \in Fin) \to \exists f (f Fn X \land \forall z \in X f (z) \in z)$
7	1	adantr	$⊢ (φ \land \neg X \in Fin) \to X ≼ ω$
8		isfinite2	$⊢ X ≺ ω \to X \in Fin$
9	8	con3i	$⊢ \neg X \in Fin \to \neg X ≺ ω$
10	9	adantl	$⊢ (φ \land \neg X \in Fin) \to \neg X ≺ ω$
11	7 10	jca	$⊢ (φ \land \neg X \in Fin) \to (X ≼ ω \land \neg X ≺ ω)$
12		bren2	$⊢ X \approx ω \leftrightarrow (X ≼ ω \land \neg X ≺ ω)$
13	11 12	sylibr	$⊢ (φ \land \neg X \in Fin) \to X \approx ω$
14		ctex	$⊢ X ≼ ω \to X \in V$
15	1 14	syl	$⊢ φ \to X \in V$
16	15	adantr	$⊢ (φ \land X \approx ω) \to X \in V$
17		simpr	$⊢ (φ \land X \approx ω) \to X \approx ω$
18		breq1	$⊢ x = X \to (x \approx ω \leftrightarrow X \approx ω)$
19		raleq	$⊢ x = X \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))$
20	19	exbidv	$⊢ x = X \to (\exists g \forall z \in x (z \neq \emptyset \to g (z) \in z) \leftrightarrow \exists g \forall z \in X (z \neq \emptyset \to g (z) \in z))$
21	18 20	imbi12d	$⊢ x = X \to ((x \approx ω \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)) \leftrightarrow (X \approx ω \to \exists g \forall z \in X (z \neq \emptyset \to g (z) \in z)))$
22		ax-cc	$⊢ x \approx ω \to \exists g \forall z \in x (z \neq \emptyset \to g (z) \in z)$
23	21 22	vtoclg	$⊢ X \in V \to (X \approx ω \to \exists g \forall z \in X (z \neq \emptyset \to g (z) \in z))$
24	16 17 23	sylc	$⊢ (φ \land X \approx ω) \to \exists g \forall z \in X (z \neq \emptyset \to g (z) \in z)$
25	15	mptexd	$⊢ φ \to (z \in X ⟼ g (z)) \in V$
26	25	adantr	$⊢ (φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \to (z \in X ⟼ g (z)) \in V$
27		fvex	$⊢ g (z) \in V$
28	27	rgenw	$⊢ \forall z \in X g (z) \in V$
29		eqid	$⊢ (z \in X ⟼ g (z)) = (z \in X ⟼ g (z))$
30	29	fnmpt	$⊢ \forall z \in X g (z) \in V \to (z \in X ⟼ g (z)) Fn X$
31	28 30	ax-mp	$⊢ (z \in X ⟼ g (z)) Fn X$
32	31	a1i	$⊢ (φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \to (z \in X ⟼ g (z)) Fn X$
33		nfv	$⊢ Ⅎ z φ$
34		nfra1	$⊢ Ⅎ z \forall z \in X (z \neq \emptyset \to g (z) \in z)$
35	33 34	nfan	$⊢ Ⅎ z (φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z))$
36		id	$⊢ z \in X \to z \in X$
37	27	a1i	$⊢ z \in X \to g (z) \in V$
38	29	fvmpt2	$⊢ (z \in X \land g (z) \in V) \to (z \in X ⟼ g (z)) (z) = g (z)$
39	36 37 38	syl2anc	$⊢ z \in X \to (z \in X ⟼ g (z)) (z) = g (z)$
40	39	adantl	$⊢ ((φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \land z \in X) \to (z \in X ⟼ g (z)) (z) = g (z)$
41		rspa	$⊢ (\forall z \in X (z \neq \emptyset \to g (z) \in z) \land z \in X) \to (z \neq \emptyset \to g (z) \in z)$
42	41	adantll	$⊢ ((φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \land z \in X) \to (z \neq \emptyset \to g (z) \in z)$
43	2	adantlr	$⊢ ((φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \land z \in X) \to z \neq \emptyset$
44		id	$⊢ (z \neq \emptyset \to g (z) \in z) \to (z \neq \emptyset \to g (z) \in z)$
45	42 43 44	sylc	$⊢ ((φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \land z \in X) \to g (z) \in z$
46	40 45	eqeltrd	$⊢ ((φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \land z \in X) \to (z \in X ⟼ g (z)) (z) \in z$
47	46	ex	$⊢ (φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \to (z \in X \to (z \in X ⟼ g (z)) (z) \in z)$
48	35 47	ralrimi	$⊢ (φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \to \forall z \in X (z \in X ⟼ g (z)) (z) \in z$
49	32 48	jca	$⊢ (φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \to ((z \in X ⟼ g (z)) Fn X \land \forall z \in X (z \in X ⟼ g (z)) (z) \in z)$
50		fneq1	$⊢ f = (z \in X ⟼ g (z)) \to (f Fn X \leftrightarrow (z \in X ⟼ g (z)) Fn X)$
51		nfcv	$⊢ \underline{Ⅎ} z f$
52		nfmpt1	$⊢ \underline{Ⅎ} z (z \in X ⟼ g (z))$
53	51 52	nfeq	$⊢ Ⅎ z f = (z \in X ⟼ g (z))$
54		fveq1	$⊢ f = (z \in X ⟼ g (z)) \to f (z) = (z \in X ⟼ g (z)) (z)$
55	54	eleq1d	$⊢ f = (z \in X ⟼ g (z)) \to (f (z) \in z \leftrightarrow (z \in X ⟼ g (z)) (z) \in z)$
56	53 55	ralbid	$⊢ f = (z \in X ⟼ g (z)) \to (\forall z \in X f (z) \in z \leftrightarrow \forall z \in X (z \in X ⟼ g (z)) (z) \in z)$
57	50 56	anbi12d	$⊢ f = (z \in X ⟼ g (z)) \to ((f Fn X \land \forall z \in X f (z) \in z) \leftrightarrow ((z \in X ⟼ g (z)) Fn X \land \forall z \in X (z \in X ⟼ g (z)) (z) \in z))$
58	57	spcegv	$⊢ (z \in X ⟼ g (z)) \in V \to (((z \in X ⟼ g (z)) Fn X \land \forall z \in X (z \in X ⟼ g (z)) (z) \in z) \to \exists f (f Fn X \land \forall z \in X f (z) \in z))$
59	26 49 58	sylc	$⊢ (φ \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \to \exists f (f Fn X \land \forall z \in X f (z) \in z)$
60	59	adantlr	$⊢ ((φ \land X \approx ω) \land \forall z \in X (z \neq \emptyset \to g (z) \in z)) \to \exists f (f Fn X \land \forall z \in X f (z) \in z)$
61	60	ex	$⊢ (φ \land X \approx ω) \to (\forall z \in X (z \neq \emptyset \to g (z) \in z) \to \exists f (f Fn X \land \forall z \in X f (z) \in z))$
62	61	exlimdv	$⊢ (φ \land X \approx ω) \to (\exists g \forall z \in X (z \neq \emptyset \to g (z) \in z) \to \exists f (f Fn X \land \forall z \in X f (z) \in z))$
63	24 62	mpd	$⊢ (φ \land X \approx ω) \to \exists f (f Fn X \land \forall z \in X f (z) \in z)$
64	13 63	syldan	$⊢ (φ \land \neg X \in Fin) \to \exists f (f Fn X \land \forall z \in X f (z) \in z)$
65	6 64	pm2.61dan	$⊢ φ \to \exists f (f Fn X \land \forall z \in X f (z) \in z)$

Metamath Proof Explorer

Theorem axccdom

Proof