inffien

Description: The set of finite intersections of an infinite well-orderable set is equinumerous to the set itself. (Contributed by Mario Carneiro, 18-May-2015)

		Ref	Expression
	Assertion	inffien	$⊢ (A \in dom card \land ω ≼ A) \to fi (A) \approx A$

Proof

Step	Hyp	Ref	Expression
1		infpwfien	$⊢ (A \in dom card \land ω ≼ A) \to (𝒫 A \cap Fin) \approx A$
2		relen	$⊢ Rel \approx$
3	2	brrelex1i	$⊢ (𝒫 A \cap Fin) \approx A \to 𝒫 A \cap Fin \in V$
4	1 3	syl	$⊢ (A \in dom card \land ω ≼ A) \to 𝒫 A \cap Fin \in V$
5		difss	$⊢ (𝒫 A \cap Fin) ∖ \{\emptyset\} \subseteq 𝒫 A \cap Fin$
6		ssdomg	$⊢ 𝒫 A \cap Fin \in V \to ((𝒫 A \cap Fin) ∖ \{\emptyset\} \subseteq 𝒫 A \cap Fin \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ (𝒫 A \cap Fin))$
7	4 5 6	mpisyl	$⊢ (A \in dom card \land ω ≼ A) \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ (𝒫 A \cap Fin)$
8		domentr	$⊢ (((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ (𝒫 A \cap Fin) \land (𝒫 A \cap Fin) \approx A) \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ A$
9	7 1 8	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ A$
10		numdom	$⊢ (A \in dom card \land ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ A) \to (𝒫 A \cap Fin) ∖ \{\emptyset\} \in dom card$
11	9 10	syldan	$⊢ (A \in dom card \land ω ≼ A) \to (𝒫 A \cap Fin) ∖ \{\emptyset\} \in dom card$
12		eqid	$⊢ (x \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ x) = (x \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ x)$
13	12	fifo	$⊢ A \in dom card \to (x \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ x) : (𝒫 A \cap Fin) ∖ \{\emptyset\} \underset{onto}{⟶} fi (A)$
14	13	adantr	$⊢ (A \in dom card \land ω ≼ A) \to (x \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ x) : (𝒫 A \cap Fin) ∖ \{\emptyset\} \underset{onto}{⟶} fi (A)$
15		fodomnum	$⊢ (𝒫 A \cap Fin) ∖ \{\emptyset\} \in dom card \to ((x \in ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ⟼ ⋂ x) : (𝒫 A \cap Fin) ∖ \{\emptyset\} \underset{onto}{⟶} fi (A) \to fi (A) ≼ ((𝒫 A \cap Fin) ∖ \{\emptyset\}))$
16	11 14 15	sylc	$⊢ (A \in dom card \land ω ≼ A) \to fi (A) ≼ ((𝒫 A \cap Fin) ∖ \{\emptyset\})$
17		domtr	$⊢ (fi (A) ≼ ((𝒫 A \cap Fin) ∖ \{\emptyset\}) \land ((𝒫 A \cap Fin) ∖ \{\emptyset\}) ≼ A) \to fi (A) ≼ A$
18	16 9 17	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to fi (A) ≼ A$
19		fvex	$⊢ fi (A) \in V$
20		ssfii	$⊢ A \in dom card \to A \subseteq fi (A)$
21	20	adantr	$⊢ (A \in dom card \land ω ≼ A) \to A \subseteq fi (A)$
22		ssdomg	$⊢ fi (A) \in V \to (A \subseteq fi (A) \to A ≼ fi (A))$
23	19 21 22	mpsyl	$⊢ (A \in dom card \land ω ≼ A) \to A ≼ fi (A)$
24		sbth	$⊢ (fi (A) ≼ A \land A ≼ fi (A)) \to fi (A) \approx A$
25	18 23 24	syl2anc	$⊢ (A \in dom card \land ω ≼ A) \to fi (A) \approx A$

Metamath Proof Explorer

Theorem inffien

Proof