This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fin4en1

Description: Dedekind finite is a cardinal property. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion fin4en1 ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ FinIV → 𝐵 ∈ FinIV ) )

Proof

Step Hyp Ref Expression
1 ensym ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
2 bren ⊢ ( 𝐵 ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
3 simpr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑥 ⊊ 𝐵 ) → 𝑥 ⊊ 𝐵 )
4 f1of1 ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → 𝑓 : 𝐵 –1-1→ 𝐴 )
5 pssss ⊢ ( 𝑥 ⊊ 𝐵 → 𝑥 ⊆ 𝐵 )
6 ssid ⊢ 𝐵 ⊆ 𝐵
7 5 6 jctir ⊢ ( 𝑥 ⊊ 𝐵 → ( 𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) )
8 f1imapss ⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐴 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵 ) ) → ( ( 𝑓 “ 𝑥 ) ⊊ ( 𝑓 “ 𝐵 ) ↔ 𝑥 ⊊ 𝐵 ) )
9 4 7 8 syl2an ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑥 ⊊ 𝐵 ) → ( ( 𝑓 “ 𝑥 ) ⊊ ( 𝑓 “ 𝐵 ) ↔ 𝑥 ⊊ 𝐵 ) )
10 3 9 mpbird ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑥 ⊊ 𝐵 ) → ( 𝑓 “ 𝑥 ) ⊊ ( 𝑓 “ 𝐵 ) )
11 imadmrn ⊢ ( 𝑓 “ dom 𝑓 ) = ran 𝑓
12 f1odm ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → dom 𝑓 = 𝐵 )
13 12 imaeq2d ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( 𝑓 “ dom 𝑓 ) = ( 𝑓 “ 𝐵 ) )
14 dff1o5 ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ↔ ( 𝑓 : 𝐵 –1-1→ 𝐴 ∧ ran 𝑓 = 𝐴 ) )
15 14 simprbi ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ran 𝑓 = 𝐴 )
16 11 13 15 3eqtr3a ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( 𝑓 “ 𝐵 ) = 𝐴 )
17 16 adantr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑥 ⊊ 𝐵 ) → ( 𝑓 “ 𝐵 ) = 𝐴 )
18 17 psseq2d ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑥 ⊊ 𝐵 ) → ( ( 𝑓 “ 𝑥 ) ⊊ ( 𝑓 “ 𝐵 ) ↔ ( 𝑓 “ 𝑥 ) ⊊ 𝐴 ) )
19 10 18 mpbid ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑥 ⊊ 𝐵 ) → ( 𝑓 “ 𝑥 ) ⊊ 𝐴 )
20 19 adantrr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑓 “ 𝑥 ) ⊊ 𝐴 )
21 vex ⊢ 𝑥 ∈ V
22 21 f1imaen ⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) → ( 𝑓 “ 𝑥 ) ≈ 𝑥 )
23 4 5 22 syl2an ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑥 ⊊ 𝐵 ) → ( 𝑓 “ 𝑥 ) ≈ 𝑥 )
24 23 adantrr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑓 “ 𝑥 ) ≈ 𝑥 )
25 simprr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → 𝑥 ≈ 𝐵 )
26 entr ⊢ ( ( ( 𝑓 “ 𝑥 ) ≈ 𝑥 ∧ 𝑥 ≈ 𝐵 ) → ( 𝑓 “ 𝑥 ) ≈ 𝐵 )
27 24 25 26 syl2anc ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑓 “ 𝑥 ) ≈ 𝐵 )
28 vex ⊢ 𝑓 ∈ V
29 f1oen3g ⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ) → 𝐵 ≈ 𝐴 )
30 28 29 mpan ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → 𝐵 ≈ 𝐴 )
31 30 adantr ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → 𝐵 ≈ 𝐴 )
32 entr ⊢ ( ( ( 𝑓 “ 𝑥 ) ≈ 𝐵 ∧ 𝐵 ≈ 𝐴 ) → ( 𝑓 “ 𝑥 ) ≈ 𝐴 )
33 27 31 32 syl2anc ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ( 𝑓 “ 𝑥 ) ≈ 𝐴 )
34 fin4i ⊢ ( ( ( 𝑓 “ 𝑥 ) ⊊ 𝐴 ∧ ( 𝑓 “ 𝑥 ) ≈ 𝐴 ) → ¬ 𝐴 ∈ FinIV )
35 20 33 34 syl2anc ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) → ¬ 𝐴 ∈ FinIV )
36 35 ex ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) → ¬ 𝐴 ∈ FinIV ) )
37 36 exlimdv ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) → ¬ 𝐴 ∈ FinIV ) )
38 37 con2d ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( 𝐴 ∈ FinIV → ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) )
39 38 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( 𝐴 ∈ FinIV → ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) )
40 2 39 sylbi ⊢ ( 𝐵 ≈ 𝐴 → ( 𝐴 ∈ FinIV → ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) )
41 relen ⊢ Rel ≈
42 41 brrelex1i ⊢ ( 𝐵 ≈ 𝐴 → 𝐵 ∈ V )
43 isfin4 ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ FinIV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) )
44 42 43 syl ⊢ ( 𝐵 ≈ 𝐴 → ( 𝐵 ∈ FinIV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵 ) ) )
45 40 44 sylibrd ⊢ ( 𝐵 ≈ 𝐴 → ( 𝐴 ∈ FinIV → 𝐵 ∈ FinIV ) )
46 1 45 syl ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ FinIV → 𝐵 ∈ FinIV ) )