ufldom

Description: The ultrafilter lemma property is a cardinal invariant, so since it transfers to subsets it also transfers over set dominance. (Contributed by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	ufldom	$⊢ (X \in UFL \land Y ≼ X) \to Y \in UFL$

Proof

Step	Hyp	Ref	Expression
1		domeng	$⊢ X \in UFL \to (Y ≼ X \leftrightarrow \exists x (Y \approx x \land x \subseteq X))$
2		bren	$⊢ Y \approx x \leftrightarrow \exists f f : Y \underset{1-1 onto}{⟶} x$
3	2	biimpi	$⊢ Y \approx x \to \exists f f : Y \underset{1-1 onto}{⟶} x$
4		ssufl	$⊢ (X \in UFL \land x \subseteq X) \to x \in UFL$
5		simplr	$⊢ ((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \to x \in UFL$
6		filfbas	$⊢ g \in Fil (Y) \to g \in fBas (Y)$
7	6	adantl	$⊢ ((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \to g \in fBas (Y)$
8		f1of	$⊢ f : Y \underset{1-1 onto}{⟶} x \to f : Y ⟶ x$
9	8	ad2antrr	$⊢ ((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \to f : Y ⟶ x$
10		fmfil	$⊢ (x \in UFL \land g \in fBas (Y) \land f : Y ⟶ x) \to (x FilMap f) (g) \in Fil (x)$
11	5 7 9 10	syl3anc	$⊢ ((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \to (x FilMap f) (g) \in Fil (x)$
12		ufli	$⊢ (x \in UFL \land (x FilMap f) (g) \in Fil (x)) \to \exists y \in UFil (x) (x FilMap f) (g) \subseteq y$
13	5 11 12	syl2anc	$⊢ ((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \to \exists y \in UFil (x) (x FilMap f) (g) \subseteq y$
14		f1odm	$⊢ f : Y \underset{1-1 onto}{⟶} x \to dom f = Y$
15	14	adantr	$⊢ (f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \to dom f = Y$
16		vex	$⊢ f \in V$
17	16	dmex	$⊢ dom f \in V$
18	15 17	eqeltrrdi	$⊢ (f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \to Y \in V$
19	18	ad2antrr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to Y \in V$
20		simprl	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to y \in UFil (x)$
21		f1ocnv	$⊢ f : Y \underset{1-1 onto}{⟶} x \to f^{-1} : x \underset{1-1 onto}{⟶} Y$
22	21	ad3antrrr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to f^{-1} : x \underset{1-1 onto}{⟶} Y$
23		f1of	$⊢ f^{-1} : x \underset{1-1 onto}{⟶} Y \to f^{-1} : x ⟶ Y$
24	22 23	syl	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to f^{-1} : x ⟶ Y$
25		fmufil	$⊢ (Y \in V \land y \in UFil (x) \land f^{-1} : x ⟶ Y) \to (Y FilMap f^{-1}) (y) \in UFil (Y)$
26	19 20 24 25	syl3anc	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (Y FilMap f^{-1}) (y) \in UFil (Y)$
27		f1ococnv1	$⊢ f : Y \underset{1-1 onto}{⟶} x \to f^{-1} \circ f = {I ↾}_{Y}$
28	27	ad3antrrr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to f^{-1} \circ f = {I ↾}_{Y}$
29	28	oveq2d	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to Y FilMap (f^{-1} \circ f) = Y FilMap ({I ↾}_{Y})$
30	29	fveq1d	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (Y FilMap (f^{-1} \circ f)) (g) = (Y FilMap ({I ↾}_{Y})) (g)$
31	5	adantr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to x \in UFL$
32	7	adantr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to g \in fBas (Y)$
33	8	ad3antrrr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to f : Y ⟶ x$
34		fmco	$⊢ ((Y \in V \land x \in UFL \land g \in fBas (Y)) \land (f^{-1} : x ⟶ Y \land f : Y ⟶ x)) \to (Y FilMap (f^{-1} \circ f)) (g) = (Y FilMap f^{-1}) ((x FilMap f) (g))$
35	19 31 32 24 33 34	syl32anc	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (Y FilMap (f^{-1} \circ f)) (g) = (Y FilMap f^{-1}) ((x FilMap f) (g))$
36		simplr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to g \in Fil (Y)$
37		fmid	$⊢ g \in Fil (Y) \to (Y FilMap ({I ↾}_{Y})) (g) = g$
38	36 37	syl	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (Y FilMap ({I ↾}_{Y})) (g) = g$
39	30 35 38	3eqtr3d	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (Y FilMap f^{-1}) ((x FilMap f) (g)) = g$
40	11	adantr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (x FilMap f) (g) \in Fil (x)$
41		filfbas	$⊢ (x FilMap f) (g) \in Fil (x) \to (x FilMap f) (g) \in fBas (x)$
42	40 41	syl	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (x FilMap f) (g) \in fBas (x)$
43		ufilfil	$⊢ y \in UFil (x) \to y \in Fil (x)$
44		filfbas	$⊢ y \in Fil (x) \to y \in fBas (x)$
45	20 43 44	3syl	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to y \in fBas (x)$
46		simprr	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (x FilMap f) (g) \subseteq y$
47		fmss	$⊢ ((Y \in V \land (x FilMap f) (g) \in fBas (x) \land y \in fBas (x)) \land (f^{-1} : x ⟶ Y \land (x FilMap f) (g) \subseteq y)) \to (Y FilMap f^{-1}) ((x FilMap f) (g)) \subseteq (Y FilMap f^{-1}) (y)$
48	19 42 45 24 46 47	syl32anc	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to (Y FilMap f^{-1}) ((x FilMap f) (g)) \subseteq (Y FilMap f^{-1}) (y)$
49	39 48	eqsstrrd	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to g \subseteq (Y FilMap f^{-1}) (y)$
50		sseq2	$⊢ u = (Y FilMap f^{-1}) (y) \to (g \subseteq u \leftrightarrow g \subseteq (Y FilMap f^{-1}) (y))$
51	50	rspcev	$⊢ ((Y FilMap f^{-1}) (y) \in UFil (Y) \land g \subseteq (Y FilMap f^{-1}) (y)) \to \exists u \in UFil (Y) g \subseteq u$
52	26 49 51	syl2anc	$⊢ (((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \land (y \in UFil (x) \land (x FilMap f) (g) \subseteq y)) \to \exists u \in UFil (Y) g \subseteq u$
53	13 52	rexlimddv	$⊢ ((f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \land g \in Fil (Y)) \to \exists u \in UFil (Y) g \subseteq u$
54	53	ralrimiva	$⊢ (f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \to \forall g \in Fil (Y) \exists u \in UFil (Y) g \subseteq u$
55		isufl	$⊢ Y \in V \to (Y \in UFL \leftrightarrow \forall g \in Fil (Y) \exists u \in UFil (Y) g \subseteq u)$
56	18 55	syl	$⊢ (f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \to (Y \in UFL \leftrightarrow \forall g \in Fil (Y) \exists u \in UFil (Y) g \subseteq u)$
57	54 56	mpbird	$⊢ (f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \to Y \in UFL$
58	57	ex	$⊢ f : Y \underset{1-1 onto}{⟶} x \to (x \in UFL \to Y \in UFL)$
59	58	exlimiv	$⊢ \exists f f : Y \underset{1-1 onto}{⟶} x \to (x \in UFL \to Y \in UFL)$
60	59	imp	$⊢ (\exists f f : Y \underset{1-1 onto}{⟶} x \land x \in UFL) \to Y \in UFL$
61	3 4 60	syl2an	$⊢ (Y \approx x \land (X \in UFL \land x \subseteq X)) \to Y \in UFL$
62	61	an12s	$⊢ (X \in UFL \land (Y \approx x \land x \subseteq X)) \to Y \in UFL$
63	62	ex	$⊢ X \in UFL \to ((Y \approx x \land x \subseteq X) \to Y \in UFL)$
64	63	exlimdv	$⊢ X \in UFL \to (\exists x (Y \approx x \land x \subseteq X) \to Y \in UFL)$
65	1 64	sylbid	$⊢ X \in UFL \to (Y ≼ X \to Y \in UFL)$
66	65	imp	$⊢ (X \in UFL \land Y ≼ X) \to Y \in UFL$

Metamath Proof Explorer

Theorem ufldom

Proof