Proof of Theorem f1o00
| Step | Hyp | Ref
| Expression |
| 1 | | dff1o4 6856 |
. 2
⊢ (𝐹:∅–1-1-onto→𝐴 ↔ (𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴)) |
| 2 | | fn0 6699 |
. . . . . 6
⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) |
| 3 | 2 | biimpi 216 |
. . . . 5
⊢ (𝐹 Fn ∅ → 𝐹 = ∅) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → 𝐹 = ∅) |
| 5 | | cnveq 5884 |
. . . . . . . . . 10
⊢ (𝐹 = ∅ → ◡𝐹 = ◡∅) |
| 6 | | cnv0 6160 |
. . . . . . . . . 10
⊢ ◡∅ = ∅ |
| 7 | 5, 6 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝐹 = ∅ → ◡𝐹 = ∅) |
| 8 | 2, 7 | sylbi 217 |
. . . . . . . 8
⊢ (𝐹 Fn ∅ → ◡𝐹 = ∅) |
| 9 | 8 | fneq1d 6661 |
. . . . . . 7
⊢ (𝐹 Fn ∅ → (◡𝐹 Fn 𝐴 ↔ ∅ Fn 𝐴)) |
| 10 | 9 | biimpa 476 |
. . . . . 6
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → ∅ Fn 𝐴) |
| 11 | 10 | fndmd 6673 |
. . . . 5
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → dom ∅ = 𝐴) |
| 12 | | dm0 5931 |
. . . . 5
⊢ dom
∅ = ∅ |
| 13 | 11, 12 | eqtr3di 2792 |
. . . 4
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → 𝐴 = ∅) |
| 14 | 4, 13 | jca 511 |
. . 3
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) → (𝐹 = ∅ ∧ 𝐴 = ∅)) |
| 15 | 2 | biimpri 228 |
. . . . 5
⊢ (𝐹 = ∅ → 𝐹 Fn ∅) |
| 16 | 15 | adantr 480 |
. . . 4
⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → 𝐹 Fn ∅) |
| 17 | | eqid 2737 |
. . . . . 6
⊢ ∅ =
∅ |
| 18 | | fn0 6699 |
. . . . . 6
⊢ (∅
Fn ∅ ↔ ∅ = ∅) |
| 19 | 17, 18 | mpbir 231 |
. . . . 5
⊢ ∅
Fn ∅ |
| 20 | 7 | fneq1d 6661 |
. . . . . 6
⊢ (𝐹 = ∅ → (◡𝐹 Fn 𝐴 ↔ ∅ Fn 𝐴)) |
| 21 | | fneq2 6660 |
. . . . . 6
⊢ (𝐴 = ∅ → (∅ Fn
𝐴 ↔ ∅ Fn
∅)) |
| 22 | 20, 21 | sylan9bb 509 |
. . . . 5
⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → (◡𝐹 Fn 𝐴 ↔ ∅ Fn
∅)) |
| 23 | 19, 22 | mpbiri 258 |
. . . 4
⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → ◡𝐹 Fn 𝐴) |
| 24 | 16, 23 | jca 511 |
. . 3
⊢ ((𝐹 = ∅ ∧ 𝐴 = ∅) → (𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴)) |
| 25 | 14, 24 | impbii 209 |
. 2
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn 𝐴) ↔ (𝐹 = ∅ ∧ 𝐴 = ∅)) |
| 26 | 1, 25 | bitri 275 |
1
⊢ (𝐹:∅–1-1-onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅)) |