acndom

Description: A set with long choice sequences also has shorter choice sequences, where "shorter" here means the new index set is dominated by the old index set. (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	acndom	$⊢ A ≼ B \to (X \in \underline{AC} B \to X \in \underline{AC} A)$

Proof

Step	Hyp	Ref	Expression
1		brdomi	$⊢ A ≼ B \to \exists f f : A \underset{1-1}{⟶} B$
2		neq0	$⊢ \neg A = \emptyset \leftrightarrow \exists x x \in A$
3		simpl3	$⊢ ((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to X \in \underline{AC} B$
4		elmapi	$⊢ g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \to g : A ⟶ 𝒫 X ∖ \{\emptyset\}$
5	4	ad2antlr	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \to g : A ⟶ 𝒫 X ∖ \{\emptyset\}$
6		simpll1	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \to f : A \underset{1-1}{⟶} B$
7		f1f1orn	$⊢ f : A \underset{1-1}{⟶} B \to f : A \underset{1-1 onto}{⟶} ran f$
8		f1ocnv	$⊢ f : A \underset{1-1 onto}{⟶} ran f \to f^{-1} : ran f \underset{1-1 onto}{⟶} A$
9		f1of	$⊢ f^{-1} : ran f \underset{1-1 onto}{⟶} A \to f^{-1} : ran f ⟶ A$
10	6 7 8 9	4syl	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \to f^{-1} : ran f ⟶ A$
11	10	ffvelcdmda	$⊢ ((((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \land y \in ran f) \to f^{-1} (y) \in A$
12		simpl2	$⊢ ((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to x \in A$
13	12	ad2antrr	$⊢ ((((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \land \neg y \in ran f) \to x \in A$
14	11 13	ifclda	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \to if (y \in ran f, f^{-1} (y), x) \in A$
15	5 14	ffvelcdmd	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \to g (if (y \in ran f, f^{-1} (y), x)) \in (𝒫 X ∖ \{\emptyset\})$
16		eldifsn	$⊢ g (if (y \in ran f, f^{-1} (y), x)) \in (𝒫 X ∖ \{\emptyset\}) \leftrightarrow (g (if (y \in ran f, f^{-1} (y), x)) \in 𝒫 X \land g (if (y \in ran f, f^{-1} (y), x)) \neq \emptyset)$
17		elpwi	$⊢ g (if (y \in ran f, f^{-1} (y), x)) \in 𝒫 X \to g (if (y \in ran f, f^{-1} (y), x)) \subseteq X$
18	17	anim1i	$⊢ (g (if (y \in ran f, f^{-1} (y), x)) \in 𝒫 X \land g (if (y \in ran f, f^{-1} (y), x)) \neq \emptyset) \to (g (if (y \in ran f, f^{-1} (y), x)) \subseteq X \land g (if (y \in ran f, f^{-1} (y), x)) \neq \emptyset)$
19	16 18	sylbi	$⊢ g (if (y \in ran f, f^{-1} (y), x)) \in (𝒫 X ∖ \{\emptyset\}) \to (g (if (y \in ran f, f^{-1} (y), x)) \subseteq X \land g (if (y \in ran f, f^{-1} (y), x)) \neq \emptyset)$
20	15 19	syl	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land y \in B) \to (g (if (y \in ran f, f^{-1} (y), x)) \subseteq X \land g (if (y \in ran f, f^{-1} (y), x)) \neq \emptyset)$
21	20	ralrimiva	$⊢ ((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \forall y \in B (g (if (y \in ran f, f^{-1} (y), x)) \subseteq X \land g (if (y \in ran f, f^{-1} (y), x)) \neq \emptyset)$
22		acni2	$⊢ (X \in \underline{AC} B \land \forall y \in B (g (if (y \in ran f, f^{-1} (y), x)) \subseteq X \land g (if (y \in ran f, f^{-1} (y), x)) \neq \emptyset)) \to \exists k (k : B ⟶ X \land \forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)))$
23	3 21 22	syl2anc	$⊢ ((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \exists k (k : B ⟶ X \land \forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)))$
24		f1dm	$⊢ f : A \underset{1-1}{⟶} B \to dom f = A$
25		vex	$⊢ f \in V$
26	25	dmex	$⊢ dom f \in V$
27	24 26	eqeltrrdi	$⊢ f : A \underset{1-1}{⟶} B \to A \in V$
28	27	3ad2ant1	$⊢ (f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \to A \in V$
29	28	ad2antrr	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (k : B ⟶ X \land \forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)))) \to A \in V$
30		simpll1	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to f : A \underset{1-1}{⟶} B$
31		f1f	$⊢ f : A \underset{1-1}{⟶} B \to f : A ⟶ B$
32		frn	$⊢ f : A ⟶ B \to ran f \subseteq B$
33		ssralv	$⊢ ran f \subseteq B \to (\forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)) \to \forall y \in ran f k (y) \in g (if (y \in ran f, f^{-1} (y), x)))$
34	30 31 32 33	4syl	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to (\forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)) \to \forall y \in ran f k (y) \in g (if (y \in ran f, f^{-1} (y), x)))$
35		iftrue	$⊢ y \in ran f \to if (y \in ran f, f^{-1} (y), x) = f^{-1} (y)$
36	35	fveq2d	$⊢ y \in ran f \to g (if (y \in ran f, f^{-1} (y), x)) = g (f^{-1} (y))$
37	36	eleq2d	$⊢ y \in ran f \to (k (y) \in g (if (y \in ran f, f^{-1} (y), x)) \leftrightarrow k (y) \in g (f^{-1} (y)))$
38	37	ralbiia	$⊢ \forall y \in ran f k (y) \in g (if (y \in ran f, f^{-1} (y), x)) \leftrightarrow \forall y \in ran f k (y) \in g (f^{-1} (y))$
39	34 38	imbitrdi	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to (\forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)) \to \forall y \in ran f k (y) \in g (f^{-1} (y)))$
40		f1fn	$⊢ f : A \underset{1-1}{⟶} B \to f Fn A$
41		fveq2	$⊢ y = f (z) \to k (y) = k (f (z))$
42		2fveq3	$⊢ y = f (z) \to g (f^{-1} (y)) = g (f^{-1} (f (z)))$
43	41 42	eleq12d	$⊢ y = f (z) \to (k (y) \in g (f^{-1} (y)) \leftrightarrow k (f (z)) \in g (f^{-1} (f (z))))$
44	43	ralrn	$⊢ f Fn A \to (\forall y \in ran f k (y) \in g (f^{-1} (y)) \leftrightarrow \forall z \in A k (f (z)) \in g (f^{-1} (f (z))))$
45	30 40 44	3syl	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to (\forall y \in ran f k (y) \in g (f^{-1} (y)) \leftrightarrow \forall z \in A k (f (z)) \in g (f^{-1} (f (z))))$
46	39 45	sylibd	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to (\forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)) \to \forall z \in A k (f (z)) \in g (f^{-1} (f (z))))$
47	30 7	syl	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to f : A \underset{1-1 onto}{⟶} ran f$
48		f1ocnvfv1	$⊢ (f : A \underset{1-1 onto}{⟶} ran f \land z \in A) \to f^{-1} (f (z)) = z$
49	47 48	sylan	$⊢ ((((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \land z \in A) \to f^{-1} (f (z)) = z$
50	49	fveq2d	$⊢ ((((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \land z \in A) \to g (f^{-1} (f (z))) = g (z)$
51	50	eleq2d	$⊢ ((((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \land z \in A) \to (k (f (z)) \in g (f^{-1} (f (z))) \leftrightarrow k (f (z)) \in g (z))$
52	51	ralbidva	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to (\forall z \in A k (f (z)) \in g (f^{-1} (f (z))) \leftrightarrow \forall z \in A k (f (z)) \in g (z))$
53	46 52	sylibd	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : B ⟶ X) \to (\forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)) \to \forall z \in A k (f (z)) \in g (z))$
54	53	impr	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (k : B ⟶ X \land \forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)))) \to \forall z \in A k (f (z)) \in g (z)$
55		acnlem	$⊢ (A \in V \land \forall z \in A k (f (z)) \in g (z)) \to \exists h \forall z \in A h (z) \in g (z)$
56	29 54 55	syl2anc	$⊢ (((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (k : B ⟶ X \land \forall y \in B k (y) \in g (if (y \in ran f, f^{-1} (y), x)))) \to \exists h \forall z \in A h (z) \in g (z)$
57	23 56	exlimddv	$⊢ ((f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \exists h \forall z \in A h (z) \in g (z)$
58	57	ralrimiva	$⊢ (f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \to \forall g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists h \forall z \in A h (z) \in g (z)$
59		elex	$⊢ X \in \underline{AC} B \to X \in V$
60		isacn	$⊢ (X \in V \land A \in V) \to (X \in \underline{AC} A \leftrightarrow \forall g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists h \forall z \in A h (z) \in g (z))$
61	59 27 60	syl2anr	$⊢ (f : A \underset{1-1}{⟶} B \land X \in \underline{AC} B) \to (X \in \underline{AC} A \leftrightarrow \forall g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists h \forall z \in A h (z) \in g (z))$
62	61	3adant2	$⊢ (f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \to (X \in \underline{AC} A \leftrightarrow \forall g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists h \forall z \in A h (z) \in g (z))$
63	58 62	mpbird	$⊢ (f : A \underset{1-1}{⟶} B \land x \in A \land X \in \underline{AC} B) \to X \in \underline{AC} A$
64	63	3exp	$⊢ f : A \underset{1-1}{⟶} B \to (x \in A \to (X \in \underline{AC} B \to X \in \underline{AC} A))$
65	64	exlimdv	$⊢ f : A \underset{1-1}{⟶} B \to (\exists x x \in A \to (X \in \underline{AC} B \to X \in \underline{AC} A))$
66	2 65	biimtrid	$⊢ f : A \underset{1-1}{⟶} B \to (\neg A = \emptyset \to (X \in \underline{AC} B \to X \in \underline{AC} A))$
67		acneq	$⊢ A = \emptyset \to \underline{AC} A = \underline{AC} \emptyset$
68		0fi	$⊢ \emptyset \in Fin$
69		finacn	$⊢ \emptyset \in Fin \to \underline{AC} \emptyset = V$
70	68 69	ax-mp	$⊢ \underline{AC} \emptyset = V$
71	67 70	eqtrdi	$⊢ A = \emptyset \to \underline{AC} A = V$
72	71	eleq2d	$⊢ A = \emptyset \to (X \in \underline{AC} A \leftrightarrow X \in V)$
73	59 72	imbitrrid	$⊢ A = \emptyset \to (X \in \underline{AC} B \to X \in \underline{AC} A)$
74	66 73	pm2.61d2	$⊢ f : A \underset{1-1}{⟶} B \to (X \in \underline{AC} B \to X \in \underline{AC} A)$
75	74	exlimiv	$⊢ \exists f f : A \underset{1-1}{⟶} B \to (X \in \underline{AC} B \to X \in \underline{AC} A)$
76	1 75	syl	$⊢ A ≼ B \to (X \in \underline{AC} B \to X \in \underline{AC} A)$

Metamath Proof Explorer

Theorem acndom

Proof