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 ⊢A∈dom⁡card∧ω≼A→fi⁡A≈A

Proof

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