Metamath Proof Explorer

Theorem enfin1ai

Description: Ia-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion enfin1ai ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ FinIa → 𝐵 ∈ FinIa ) )

Proof

Step Hyp Ref Expression
1 ensym ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
2 bren ⊢ ( 𝐵 ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
3 1 2 sylib ⊢ ( 𝐴 ≈ 𝐵 → ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
4 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵 )
5 simplr ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → 𝐴 ∈ FinIa )
6 imassrn ⊢ ( 𝑓 “ 𝑥 ) ⊆ ran 𝑓
7 f1of ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → 𝑓 : 𝐵 ⟶ 𝐴 )
8 7 ad2antrr ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → 𝑓 : 𝐵 ⟶ 𝐴 )
9 8 frnd ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ran 𝑓 ⊆ 𝐴 )
10 6 9 sstrid ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑓 “ 𝑥 ) ⊆ 𝐴 )
11 fin1ai ⊢ ( ( 𝐴 ∈ FinIa ∧ ( 𝑓 “ 𝑥 ) ⊆ 𝐴 ) → ( ( 𝑓 “ 𝑥 ) ∈ Fin ∨ ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) ∈ Fin ) )
12 5 10 11 syl2anc ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑓 “ 𝑥 ) ∈ Fin ∨ ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) ∈ Fin ) )
13 f1of1 ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → 𝑓 : 𝐵 –1-1→ 𝐴 )
14 13 ad2antrr ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → 𝑓 : 𝐵 –1-1→ 𝐴 )
15 simpr ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ⊆ 𝐵 )
16 vex ⊢ 𝑥 ∈ V
17 16 a1i ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ∈ V )
18 f1imaeng ⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐴 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ V ) → ( 𝑓 “ 𝑥 ) ≈ 𝑥 )
19 14 15 17 18 syl3anc ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑓 “ 𝑥 ) ≈ 𝑥 )
20 enfi ⊢ ( ( 𝑓 “ 𝑥 ) ≈ 𝑥 → ( ( 𝑓 “ 𝑥 ) ∈ Fin ↔ 𝑥 ∈ Fin ) )
21 19 20 syl ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑓 “ 𝑥 ) ∈ Fin ↔ 𝑥 ∈ Fin ) )
22 df-f1 ⊢ ( 𝑓 : 𝐵 –1-1→ 𝐴 ↔ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Fun ◡ 𝑓 ) )
23 22 simprbi ⊢ ( 𝑓 : 𝐵 –1-1→ 𝐴 → Fun ◡ 𝑓 )
24 imadif ⊢ ( Fun ◡ 𝑓 → ( 𝑓 “ ( 𝐵 ∖ 𝑥 ) ) = ( ( 𝑓 “ 𝐵 ) ∖ ( 𝑓 “ 𝑥 ) ) )
25 14 23 24 3syl ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑓 “ ( 𝐵 ∖ 𝑥 ) ) = ( ( 𝑓 “ 𝐵 ) ∖ ( 𝑓 “ 𝑥 ) ) )
26 f1ofo ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → 𝑓 : 𝐵 –onto→ 𝐴 )
27 foima ⊢ ( 𝑓 : 𝐵 –onto→ 𝐴 → ( 𝑓 “ 𝐵 ) = 𝐴 )
28 26 27 syl ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( 𝑓 “ 𝐵 ) = 𝐴 )
29 28 ad2antrr ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑓 “ 𝐵 ) = 𝐴 )
30 29 difeq1d ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝑓 “ 𝐵 ) ∖ ( 𝑓 “ 𝑥 ) ) = ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) )
31 25 30 eqtrd ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑓 “ ( 𝐵 ∖ 𝑥 ) ) = ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) )
32 difssd ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵 )
33 vex ⊢ 𝑓 ∈ V
34 7 adantr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) → 𝑓 : 𝐵 ⟶ 𝐴 )
35 dmfex ⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝐵 ∈ V )
36 33 34 35 sylancr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) → 𝐵 ∈ V )
37 36 adantr ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → 𝐵 ∈ V )
38 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ 𝑥 ) ∈ V )
39 37 38 syl ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐵 ∖ 𝑥 ) ∈ V )
40 f1imaeng ⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐴 ∧ ( 𝐵 ∖ 𝑥 ) ⊆ 𝐵 ∧ ( 𝐵 ∖ 𝑥 ) ∈ V ) → ( 𝑓 “ ( 𝐵 ∖ 𝑥 ) ) ≈ ( 𝐵 ∖ 𝑥 ) )
41 14 32 39 40 syl3anc ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑓 “ ( 𝐵 ∖ 𝑥 ) ) ≈ ( 𝐵 ∖ 𝑥 ) )
42 31 41 eqbrtrrd ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) ≈ ( 𝐵 ∖ 𝑥 ) )
43 enfi ⊢ ( ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) ≈ ( 𝐵 ∖ 𝑥 ) → ( ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) ∈ Fin ↔ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) )
44 42 43 syl ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) ∈ Fin ↔ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) )
45 21 44 orbi12d ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( ( ( 𝑓 “ 𝑥 ) ∈ Fin ∨ ( 𝐴 ∖ ( 𝑓 “ 𝑥 ) ) ∈ Fin ) ↔ ( 𝑥 ∈ Fin ∨ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) ) )
46 12 45 mpbid ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑥 ∈ Fin ∨ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) )
47 4 46 sylan2 ⊢ ( ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) ∧ 𝑥 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ Fin ∨ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) )
48 47 ralrimiva ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) → ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑥 ∈ Fin ∨ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) )
49 isfin1a ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ FinIa ↔ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑥 ∈ Fin ∨ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) ) )
50 36 49 syl ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) → ( 𝐵 ∈ FinIa ↔ ∀ 𝑥 ∈ 𝒫 𝐵 ( 𝑥 ∈ Fin ∨ ( 𝐵 ∖ 𝑥 ) ∈ Fin ) ) )
51 48 50 mpbird ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝐴 ∈ FinIa ) → 𝐵 ∈ FinIa )
52 51 ex ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( 𝐴 ∈ FinIa → 𝐵 ∈ FinIa ) )
53 52 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( 𝐴 ∈ FinIa → 𝐵 ∈ FinIa ) )
54 3 53 syl ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ FinIa → 𝐵 ∈ FinIa ) )