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 ) )