fictb

Description: A set is countable iff its collection of finite intersections is countable. (Contributed by Jeff Hankins, 24-Aug-2009) (Proof shortened by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	fictb	$⊢ A \in B \to (A ≼ ω \leftrightarrow fi (A) ≼ ω)$

Proof

Step	Hyp	Ref	Expression
1		brdomi	$⊢ A ≼ ω \to \exists f f : A \underset{1-1}{⟶} ω$
2	1	adantl	$⊢ (A \in B \land A ≼ ω) \to \exists f f : A \underset{1-1}{⟶} ω$
3		reldom	$⊢ Rel ≼$
4	3	brrelex2i	$⊢ A ≼ ω \to ω \in V$
5		omelon2	$⊢ ω \in V \to ω \in On$
6	5	ad2antlr	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to ω \in On$
7		pwexg	$⊢ A \in B \to 𝒫 A \in V$
8	7	ad2antrr	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to 𝒫 A \in V$
9		inex1g	$⊢ 𝒫 A \in V \to 𝒫 A \cap Fin \in V$
10	8 9	syl	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to 𝒫 A \cap Fin \in V$
11		difss	$⊢ (𝒫 A \cap Fin) ∖ \{\emptyset\} \subseteq 𝒫 A \cap Fin$
12		ssdomg	$⊢ 𝒫 A \cap Fin \in V \to ((𝒫 A \cap Fin) ∖ \{\emptyset\} \subseteq 𝒫 A \cap Fin \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ (𝒫 A \cap Fin))$
13	10 11 12	mpisyl	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ (𝒫 A \cap Fin)$
14		f1f1orn	$⊢ f : A \underset{1-1}{⟶} ω \to f : A \underset{1-1 onto}{⟶} ran f$
15	14	adantl	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to f : A \underset{1-1 onto}{⟶} ran f$
16		f1opwfi	$⊢ f : A \underset{1-1 onto}{⟶} ran f \to (x \in (𝒫 A \cap Fin) ⟼ f [x]) : 𝒫 A \cap Fin \underset{1-1 onto}{⟶} 𝒫 ran f \cap Fin$
17	15 16	syl	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (x \in (𝒫 A \cap Fin) ⟼ f [x]) : 𝒫 A \cap Fin \underset{1-1 onto}{⟶} 𝒫 ran f \cap Fin$
18		f1oeng	$⊢ (𝒫 A \cap Fin \in V \land (x \in (𝒫 A \cap Fin) ⟼ f [x]) : 𝒫 A \cap Fin \underset{1-1 onto}{⟶} 𝒫 ran f \cap Fin) \to (𝒫 A \cap Fin) \approx (𝒫 ran f \cap Fin)$
19	10 17 18	syl2anc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (𝒫 A \cap Fin) \approx (𝒫 ran f \cap Fin)$
20		pwexg	$⊢ ω \in V \to 𝒫 ω \in V$
21	20	ad2antlr	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to 𝒫 ω \in V$
22		inex1g	$⊢ 𝒫 ω \in V \to 𝒫 ω \cap Fin \in V$
23	21 22	syl	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to 𝒫 ω \cap Fin \in V$
24		f1f	$⊢ f : A \underset{1-1}{⟶} ω \to f : A ⟶ ω$
25	24	frnd	$⊢ f : A \underset{1-1}{⟶} ω \to ran f \subseteq ω$
26	25	adantl	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to ran f \subseteq ω$
27	26	sspwd	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to 𝒫 ran f \subseteq 𝒫 ω$
28	27	ssrind	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to 𝒫 ran f \cap Fin \subseteq 𝒫 ω \cap Fin$
29		ssdomg	$⊢ 𝒫 ω \cap Fin \in V \to (𝒫 ran f \cap Fin \subseteq 𝒫 ω \cap Fin \to (𝒫 ran f \cap Fin) ≼ (𝒫 ω \cap Fin))$
30	23 28 29	sylc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (𝒫 ran f \cap Fin) ≼ (𝒫 ω \cap Fin)$
31		sneq	$⊢ f = z \to \{f\} = \{z\}$
32		pweq	$⊢ f = z \to 𝒫 f = 𝒫 z$
33	31 32	xpeq12d	$⊢ f = z \to \{f\} \times 𝒫 f = \{z\} \times 𝒫 z$
34	33	cbviunv	$⊢ ⋃_{f \in x} (\{f\} \times 𝒫 f) = ⋃_{z \in x} (\{z\} \times 𝒫 z)$
35		iuneq1	$⊢ x = y \to ⋃_{z \in x} (\{z\} \times 𝒫 z) = ⋃_{z \in y} (\{z\} \times 𝒫 z)$
36	34 35	syl5eq	$⊢ x = y \to ⋃_{f \in x} (\{f\} \times 𝒫 f) = ⋃_{z \in y} (\{z\} \times 𝒫 z)$
37	36	fveq2d	$⊢ x = y \to card (⋃_{f \in x} (\{f\} \times 𝒫 f)) = card (⋃_{z \in y} (\{z\} \times 𝒫 z))$
38	37	cbvmptv	$⊢ (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{f \in x} (\{f\} \times 𝒫 f))) = (y \in (𝒫 ω \cap Fin) ⟼ card (⋃_{z \in y} (\{z\} \times 𝒫 z)))$
39	38	ackbij1	$⊢ (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{f \in x} (\{f\} \times 𝒫 f))) : 𝒫 ω \cap Fin \underset{1-1 onto}{⟶} ω$
40		f1oeng	$⊢ (𝒫 ω \cap Fin \in V \land (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{f \in x} (\{f\} \times 𝒫 f))) : 𝒫 ω \cap Fin \underset{1-1 onto}{⟶} ω) \to (𝒫 ω \cap Fin) \approx ω$
41	23 39 40	sylancl	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (𝒫 ω \cap Fin) \approx ω$
42		domentr	$⊢ ((𝒫 ran f \cap Fin) ≼ (𝒫 ω \cap Fin) \land (𝒫 ω \cap Fin) \approx ω) \to (𝒫 ran f \cap Fin) ≼ ω$
43	30 41 42	syl2anc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (𝒫 ran f \cap Fin) ≼ ω$
44		endomtr	$⊢ ((𝒫 A \cap Fin) \approx (𝒫 ran f \cap Fin) \land (𝒫 ran f \cap Fin) ≼ ω) \to (𝒫 A \cap Fin) ≼ ω$
45	19 43 44	syl2anc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (𝒫 A \cap Fin) ≼ ω$
46		domtr	$⊢ (((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ (𝒫 A \cap Fin) \land (𝒫 A \cap Fin) ≼ ω) \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ ω$
47	13 45 46	syl2anc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ ω$
48		ondomen	$⊢ (ω \in On \land ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ ω) \to (𝒫 A \cap Fin) ∖ \{\emptyset\} \in dom card$
49	6 47 48	syl2anc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (𝒫 A \cap Fin) ∖ \{\emptyset\} \in dom card$
50		eqid	$⊢ (y \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ y) = (y \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ y)$
51	50	fifo	$⊢ A \in B \to (y \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ y) : (𝒫 A \cap Fin) ∖ \{\emptyset\} \underset{onto}{⟶} fi (A)$
52	51	ad2antrr	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to (y \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ y) : (𝒫 A \cap Fin) ∖ \{\emptyset\} \underset{onto}{⟶} fi (A)$
53		fodomnum	$⊢ (𝒫 A \cap Fin) ∖ \{\emptyset\} \in dom card \to ((y \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ y) : (𝒫 A \cap Fin) ∖ \{\emptyset\} \underset{onto}{⟶} fi (A) \to fi (A) ≼ ((𝒫 A \cap Fin) ∖ \{\emptyset\}))$
54	49 52 53	sylc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to fi (A) ≼ ((𝒫 A \cap Fin) ∖ \{\emptyset\})$
55		domtr	$⊢ (fi (A) ≼ ((𝒫 A \cap Fin) ∖ \{\emptyset\}) \land ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ ω) \to fi (A) ≼ ω$
56	54 47 55	syl2anc	$⊢ ((A \in B \land ω \in V) \land f : A \underset{1-1}{⟶} ω) \to fi (A) ≼ ω$
57	56	ex	$⊢ (A \in B \land ω \in V) \to (f : A \underset{1-1}{⟶} ω \to fi (A) ≼ ω)$
58	57	exlimdv	$⊢ (A \in B \land ω \in V) \to (\exists f f : A \underset{1-1}{⟶} ω \to fi (A) ≼ ω)$
59	4 58	sylan2	$⊢ (A \in B \land A ≼ ω) \to (\exists f f : A \underset{1-1}{⟶} ω \to fi (A) ≼ ω)$
60	2 59	mpd	$⊢ (A \in B \land A ≼ ω) \to fi (A) ≼ ω$
61	60	ex	$⊢ A \in B \to (A ≼ ω \to fi (A) ≼ ω)$
62		fvex	$⊢ fi (A) \in V$
63		ssfii	$⊢ A \in B \to A \subseteq fi (A)$
64		ssdomg	$⊢ fi (A) \in V \to (A \subseteq fi (A) \to A ≼ fi (A))$
65	62 63 64	mpsyl	$⊢ A \in B \to A ≼ fi (A)$
66		domtr	$⊢ (A ≼ fi (A) \land fi (A) ≼ ω) \to A ≼ ω$
67	66	ex	$⊢ A ≼ fi (A) \to (fi (A) ≼ ω \to A ≼ ω)$
68	65 67	syl	$⊢ A \in B \to (fi (A) ≼ ω \to A ≼ ω)$
69	61 68	impbid	$⊢ A \in B \to (A ≼ ω \leftrightarrow fi (A) ≼ ω)$

Metamath Proof Explorer

Theorem fictb

Proof