acndom2

Description: A set smaller than one with choice sequences of length A also has choice sequences of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		brdomi	$⊢ X ≼ Y \to \exists f f : X \underset{1-1}{⟶} Y$
2		simplr	$⊢ ((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to Y \in \underline{AC} A$
3		imassrn	$⊢ f [g (x)] \subseteq ran f$
4		simplll	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to f : X \underset{1-1}{⟶} Y$
5		f1f	$⊢ f : X \underset{1-1}{⟶} Y \to f : X ⟶ Y$
6		frn	$⊢ f : X ⟶ Y \to ran f \subseteq Y$
7	4 5 6	3syl	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to ran f \subseteq Y$
8	3 7	sstrid	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to f [g (x)] \subseteq Y$
9		elmapi	$⊢ g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \to g : A ⟶ 𝒫 X ∖ \{\emptyset\}$
10	9	adantl	$⊢ ((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to g : A ⟶ 𝒫 X ∖ \{\emptyset\}$
11	10	ffvelrnda	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to g (x) \in (𝒫 X ∖ \{\emptyset\})$
12	11	eldifad	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to g (x) \in 𝒫 X$
13	12	elpwid	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to g (x) \subseteq X$
14		f1dm	$⊢ f : X \underset{1-1}{⟶} Y \to dom f = X$
15	4 14	syl	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to dom f = X$
16	13 15	sseqtrrd	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to g (x) \subseteq dom f$
17		sseqin2	$⊢ g (x) \subseteq dom f \leftrightarrow dom f \cap g (x) = g (x)$
18	16 17	sylib	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to dom f \cap g (x) = g (x)$
19		eldifsni	$⊢ g (x) \in (𝒫 X ∖ \{\emptyset\}) \to g (x) \neq \emptyset$
20	11 19	syl	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to g (x) \neq \emptyset$
21	18 20	eqnetrd	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to dom f \cap g (x) \neq \emptyset$
22		imadisj	$⊢ f [g (x)] = \emptyset \leftrightarrow dom f \cap g (x) = \emptyset$
23	22	necon3bii	$⊢ f [g (x)] \neq \emptyset \leftrightarrow dom f \cap g (x) \neq \emptyset$
24	21 23	sylibr	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to f [g (x)] \neq \emptyset$
25	8 24	jca	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land x \in A) \to (f [g (x)] \subseteq Y \land f [g (x)] \neq \emptyset)$
26	25	ralrimiva	$⊢ ((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \forall x \in A (f [g (x)] \subseteq Y \land f [g (x)] \neq \emptyset)$
27		acni2	$⊢ (Y \in \underline{AC} A \land \forall x \in A (f [g (x)] \subseteq Y \land f [g (x)] \neq \emptyset)) \to \exists k (k : A ⟶ Y \land \forall x \in A k (x) \in f [g (x)])$
28	2 26 27	syl2anc	$⊢ ((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \exists k (k : A ⟶ Y \land \forall x \in A k (x) \in f [g (x)])$
29		acnrcl	$⊢ Y \in \underline{AC} A \to A \in V$
30	29	ad3antlr	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (k : A ⟶ Y \land \forall x \in A k (x) \in f [g (x)])) \to A \in V$
31		simp-4l	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to f : X \underset{1-1}{⟶} Y$
32		f1f1orn	$⊢ f : X \underset{1-1}{⟶} Y \to f : X \underset{1-1 onto}{⟶} ran f$
33	31 32	syl	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to f : X \underset{1-1 onto}{⟶} ran f$
34		simprr	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to k (x) \in f [g (x)]$
35	3 34	sseldi	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to k (x) \in ran f$
36		f1ocnvfv2	$⊢ (f : X \underset{1-1 onto}{⟶} ran f \land k (x) \in ran f) \to f (f^{-1} (k (x))) = k (x)$
37	33 35 36	syl2anc	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to f (f^{-1} (k (x))) = k (x)$
38	37 34	eqeltrd	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to f (f^{-1} (k (x))) \in f [g (x)]$
39		f1ocnv	$⊢ f : X \underset{1-1 onto}{⟶} ran f \to f^{-1} : ran f \underset{1-1 onto}{⟶} X$
40		f1of	$⊢ f^{-1} : ran f \underset{1-1 onto}{⟶} X \to f^{-1} : ran f ⟶ X$
41	33 39 40	3syl	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to f^{-1} : ran f ⟶ X$
42	41 35	ffvelrnd	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to f^{-1} (k (x)) \in X$
43	13	ad2ant2r	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to g (x) \subseteq X$
44		f1elima	$⊢ (f : X \underset{1-1}{⟶} Y \land f^{-1} (k (x)) \in X \land g (x) \subseteq X) \to (f (f^{-1} (k (x))) \in f [g (x)] \leftrightarrow f^{-1} (k (x)) \in g (x))$
45	31 42 43 44	syl3anc	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to (f (f^{-1} (k (x))) \in f [g (x)] \leftrightarrow f^{-1} (k (x)) \in g (x))$
46	38 45	mpbid	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land (x \in A \land k (x) \in f [g (x)])) \to f^{-1} (k (x)) \in g (x)$
47	46	expr	$⊢ ((((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \land x \in A) \to (k (x) \in f [g (x)] \to f^{-1} (k (x)) \in g (x))$
48	47	ralimdva	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land k : A ⟶ Y) \to (\forall x \in A k (x) \in f [g (x)] \to \forall x \in A f^{-1} (k (x)) \in g (x))$
49	48	impr	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (k : A ⟶ Y \land \forall x \in A k (x) \in f [g (x)])) \to \forall x \in A f^{-1} (k (x)) \in g (x)$
50		acnlem	$⊢ (A \in V \land \forall x \in A f^{-1} (k (x)) \in g (x)) \to \exists h \forall x \in A h (x) \in g (x)$
51	30 49 50	syl2anc	$⊢ (((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \land (k : A ⟶ Y \land \forall x \in A k (x) \in f [g (x)])) \to \exists h \forall x \in A h (x) \in g (x)$
52	28 51	exlimddv	$⊢ ((f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \land g \in ({(𝒫 X ∖ \{\emptyset\})}^{A})) \to \exists h \forall x \in A h (x) \in g (x)$
53	52	ralrimiva	$⊢ (f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \to \forall g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists h \forall x \in A h (x) \in g (x)$
54		vex	$⊢ f \in V$
55	54	dmex	$⊢ dom f \in V$
56	14 55	eqeltrrdi	$⊢ f : X \underset{1-1}{⟶} Y \to X \in V$
57		isacn	$⊢ (X \in V \land A \in V) \to (X \in \underline{AC} A \leftrightarrow \forall g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists h \forall x \in A h (x) \in g (x))$
58	56 29 57	syl2an	$⊢ (f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \to (X \in \underline{AC} A \leftrightarrow \forall g \in ({(𝒫 X ∖ \{\emptyset\})}^{A}) \exists h \forall x \in A h (x) \in g (x))$
59	53 58	mpbird	$⊢ (f : X \underset{1-1}{⟶} Y \land Y \in \underline{AC} A) \to X \in \underline{AC} A$
60	59	ex	$⊢ f : X \underset{1-1}{⟶} Y \to (Y \in \underline{AC} A \to X \in \underline{AC} A)$
61	60	exlimiv	$⊢ \exists f f : X \underset{1-1}{⟶} Y \to (Y \in \underline{AC} A \to X \in \underline{AC} A)$
62	1 61	syl	$⊢ X ≼ Y \to (Y \in \underline{AC} A \to X \in \underline{AC} A)$

Metamath Proof Explorer

Theorem acndom2

Proof