Metamath Proof Explorer

Theorem f1finf1oOLD

Description: Obsolete version of f1finf1o as of 4-Jan-2025. (Contributed by Jeff Madsen, 5-Jun-2010) (Revised by Mario Carneiro, 27-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion f1finf1oOLD ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
2 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
3 2 adantl ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
4 3 ffnd ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 Fn 𝐴 )
5 simpll ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≈ 𝐵 )
6 3 frnd ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ran 𝐹 ⊆ 𝐵 )
7 df-pss ⊢ ( ran 𝐹 ⊊ 𝐵 ↔ ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ≠ 𝐵 ) )
8 7 baib ⊢ ( ran 𝐹 ⊆ 𝐵 → ( ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵 ) )
9 6 8 syl ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵 ) )
10 simplr ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐵 ∈ Fin )
11 relen ⊢ Rel ≈
12 11 brrelex1i ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
13 5 12 syl ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ∈ V )
14 10 13 elmapd ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
15 3 14 mpbird ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) )
16 f1f1orn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
17 16 adantl ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
18 f1oen3g ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ) → 𝐴 ≈ ran 𝐹 )
19 15 17 18 syl2anc ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≈ ran 𝐹 )
20 php3 ⊢ ( ( 𝐵 ∈ Fin ∧ ran 𝐹 ⊊ 𝐵 ) → ran 𝐹 ≺ 𝐵 )
21 20 ex ⊢ ( 𝐵 ∈ Fin → ( ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵 ) )
22 10 21 syl ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵 ) )
23 ensdomtr ⊢ ( ( 𝐴 ≈ ran 𝐹 ∧ ran 𝐹 ≺ 𝐵 ) → 𝐴 ≺ 𝐵 )
24 19 22 23 syl6an ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ⊊ 𝐵 → 𝐴 ≺ 𝐵 ) )
25 sdomnen ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
26 24 25 syl6 ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ⊊ 𝐵 → ¬ 𝐴 ≈ 𝐵 ) )
27 9 26 sylbird ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ran 𝐹 ≠ 𝐵 → ¬ 𝐴 ≈ 𝐵 ) )
28 27 necon4ad ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝐴 ≈ 𝐵 → ran 𝐹 = 𝐵 ) )
29 5 28 mpd ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ran 𝐹 = 𝐵 )
30 df-fo ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ) )
31 4 29 30 sylanbrc ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
32 df-f1o ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) )
33 1 31 32 sylanbrc ⊢ ( ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
34 33 ex ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )
35 f1of1 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 )
36 34 35 impbid1 ⊢ ( ( 𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) )