Proof of Theorem f1finf1o
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . 4
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1→𝐵) |
2 | | f1f 6014 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
3 | 2 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴⟶𝐵) |
4 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹 Fn 𝐴) |
6 | | simpll 786 |
. . . . . 6
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≈ 𝐵) |
7 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
8 | 3, 7 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → ran 𝐹 ⊆ 𝐵) |
9 | | df-pss 3556 |
. . . . . . . . . 10
⊢ (ran
𝐹 ⊊ 𝐵 ↔ (ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ≠ 𝐵)) |
10 | 9 | baib 942 |
. . . . . . . . 9
⊢ (ran
𝐹 ⊆ 𝐵 → (ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵)) |
11 | 8, 10 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 ↔ ran 𝐹 ≠ 𝐵)) |
12 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐵 ∈ Fin) |
13 | | relen 7846 |
. . . . . . . . . . . . . . 15
⊢ Rel
≈ |
14 | 13 | brrelexi 5082 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ≈ 𝐵 → 𝐴 ∈ V) |
15 | 6, 14 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ∈ V) |
16 | 12, 15 | elmapd 7758 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ (𝐵 ↑𝑚 𝐴) ↔ 𝐹:𝐴⟶𝐵)) |
17 | 3, 16 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹 ∈ (𝐵 ↑𝑚 𝐴)) |
18 | | f1f1orn 6061 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
19 | 18 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1-onto→ran
𝐹) |
20 | | f1oen3g 7857 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐵 ↑𝑚 𝐴) ∧ 𝐹:𝐴–1-1-onto→ran
𝐹) → 𝐴 ≈ ran 𝐹) |
21 | 17, 19, 20 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≈ ran 𝐹) |
22 | | php3 8031 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Fin ∧ ran 𝐹 ⊊ 𝐵) → ran 𝐹 ≺ 𝐵) |
23 | 22 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Fin → (ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵)) |
24 | 12, 23 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → ran 𝐹 ≺ 𝐵)) |
25 | | ensdomtr 7981 |
. . . . . . . . . 10
⊢ ((𝐴 ≈ ran 𝐹 ∧ ran 𝐹 ≺ 𝐵) → 𝐴 ≺ 𝐵) |
26 | 21, 24, 25 | syl6an 566 |
. . . . . . . . 9
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → 𝐴 ≺ 𝐵)) |
27 | | sdomnen 7870 |
. . . . . . . . 9
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) |
28 | 26, 27 | syl6 34 |
. . . . . . . 8
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ⊊ 𝐵 → ¬ 𝐴 ≈ 𝐵)) |
29 | 11, 28 | sylbird 249 |
. . . . . . 7
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (ran 𝐹 ≠ 𝐵 → ¬ 𝐴 ≈ 𝐵)) |
30 | 29 | necon4ad 2801 |
. . . . . 6
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → (𝐴 ≈ 𝐵 → ran 𝐹 = 𝐵)) |
31 | 6, 30 | mpd 15 |
. . . . 5
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → ran 𝐹 = 𝐵) |
32 | | df-fo 5810 |
. . . . 5
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) |
33 | 5, 31, 32 | sylanbrc 695 |
. . . 4
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–onto→𝐵) |
34 | | df-f1o 5811 |
. . . 4
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)) |
35 | 1, 33, 34 | sylanbrc 695 |
. . 3
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐹:𝐴–1-1-onto→𝐵) |
36 | 35 | ex 449 |
. 2
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→𝐵)) |
37 | | f1of1 6049 |
. 2
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵) |
38 | 36, 37 | impbid1 214 |
1
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) |