Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( fi ‘ 𝐴 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 infpwfien ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ≈ 𝐴 )
2 relen ⊢ Rel ≈
3 2 brrelex1i ⊢ ( ( 𝒫 𝐴 ∩ Fin ) ≈ 𝐴 → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
4 1 3 syl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
5 difss ⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ⊆ ( 𝒫 𝐴 ∩ Fin )
6 ssdomg ⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∈ V → ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ⊆ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ( 𝒫 𝐴 ∩ Fin ) ) )
7 4 5 6 mpisyl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ( 𝒫 𝐴 ∩ Fin ) )
8 domentr ⊢ ( ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝒫 𝐴 ∩ Fin ) ≈ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ 𝐴 )
9 7 1 8 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ 𝐴 )
10 numdom ⊢ ( ( 𝐴 ∈ dom card ∧ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card )
11 9 10 syldan ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card )
12 eqid ⊢ ( 𝑥 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑥 ) = ( 𝑥 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑥 )
13 12 fifo ⊢ ( 𝐴 ∈ dom card → ( 𝑥 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑥 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )
14 13 adantr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑥 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑥 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )
15 fodomnum ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card → ( ( 𝑥 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑥 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) → ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ) )
16 11 14 15 sylc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) )
17 domtr ⊢ ( ( ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∧ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ 𝐴 ) → ( fi ‘ 𝐴 ) ≼ 𝐴 )
18 16 9 17 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( fi ‘ 𝐴 ) ≼ 𝐴 )
19 fvex ⊢ ( fi ‘ 𝐴 ) ∈ V
20 ssfii ⊢ ( 𝐴 ∈ dom card → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
21 20 adantr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
22 ssdomg ⊢ ( ( fi ‘ 𝐴 ) ∈ V → ( 𝐴 ⊆ ( fi ‘ 𝐴 ) → 𝐴 ≼ ( fi ‘ 𝐴 ) ) )
23 19 21 22 mpsyl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ≼ ( fi ‘ 𝐴 ) )
24 sbth ⊢ ( ( ( fi ‘ 𝐴 ) ≼ 𝐴 ∧ 𝐴 ≼ ( fi ‘ 𝐴 ) ) → ( fi ‘ 𝐴 ) ≈ 𝐴 )
25 18 23 24 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( fi ‘ 𝐴 ) ≈ 𝐴 )