Proof of Theorem f1o00
Step | Hyp | Ref
| Expression |
1 | | dff1o4 5077 |
. 2
⊢ (𝐹:∅–1-1-onto→A ↔
(𝐹 Fn ∅ ∧ ◡𝐹 Fn A)) |
2 | | fn0 4961 |
. . . . . 6
⊢ (𝐹 Fn ∅ ↔ 𝐹 = ∅) |
3 | 2 | biimpi 113 |
. . . . 5
⊢ (𝐹 Fn ∅ → 𝐹 = ∅) |
4 | 3 | adantr 261 |
. . . 4
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn A) → 𝐹 = ∅) |
5 | | dm0 4492 |
. . . . 5
⊢ dom
∅ = ∅ |
6 | | cnveq 4452 |
. . . . . . . . . 10
⊢ (𝐹 = ∅ → ◡𝐹 = ◡∅) |
7 | | cnv0 4670 |
. . . . . . . . . 10
⊢ ◡∅ = ∅ |
8 | 6, 7 | syl6eq 2085 |
. . . . . . . . 9
⊢ (𝐹 = ∅ → ◡𝐹 = ∅) |
9 | 2, 8 | sylbi 114 |
. . . . . . . 8
⊢ (𝐹 Fn ∅ → ◡𝐹 = ∅) |
10 | 9 | fneq1d 4932 |
. . . . . . 7
⊢ (𝐹 Fn ∅ → (◡𝐹 Fn A
↔ ∅ Fn A)) |
11 | 10 | biimpa 280 |
. . . . . 6
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn A) → ∅ Fn A) |
12 | | fndm 4941 |
. . . . . 6
⊢ (∅
Fn A → dom ∅ = A) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn A) → dom ∅ = A) |
14 | 5, 13 | syl5reqr 2084 |
. . . 4
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn A) → A =
∅) |
15 | 4, 14 | jca 290 |
. . 3
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn A) → (𝐹 = ∅ ∧ A =
∅)) |
16 | 2 | biimpri 124 |
. . . . 5
⊢ (𝐹 = ∅ → 𝐹 Fn ∅) |
17 | 16 | adantr 261 |
. . . 4
⊢ ((𝐹 = ∅ ∧ A = ∅)
→ 𝐹 Fn
∅) |
18 | | eqid 2037 |
. . . . . 6
⊢ ∅ =
∅ |
19 | | fn0 4961 |
. . . . . 6
⊢ (∅
Fn ∅ ↔ ∅ = ∅) |
20 | 18, 19 | mpbir 134 |
. . . . 5
⊢ ∅
Fn ∅ |
21 | 8 | fneq1d 4932 |
. . . . . 6
⊢ (𝐹 = ∅ → (◡𝐹 Fn A
↔ ∅ Fn A)) |
22 | | fneq2 4931 |
. . . . . 6
⊢ (A = ∅ → (∅ Fn A ↔ ∅ Fn ∅)) |
23 | 21, 22 | sylan9bb 435 |
. . . . 5
⊢ ((𝐹 = ∅ ∧ A = ∅)
→ (◡𝐹 Fn A
↔ ∅ Fn ∅)) |
24 | 20, 23 | mpbiri 157 |
. . . 4
⊢ ((𝐹 = ∅ ∧ A = ∅)
→ ◡𝐹 Fn A) |
25 | 17, 24 | jca 290 |
. . 3
⊢ ((𝐹 = ∅ ∧ A = ∅)
→ (𝐹 Fn ∅ ∧ ◡𝐹 Fn A)) |
26 | 15, 25 | impbii 117 |
. 2
⊢ ((𝐹 Fn ∅ ∧ ◡𝐹 Fn A) ↔ (𝐹 = ∅ ∧ A =
∅)) |
27 | 1, 26 | bitri 173 |
1
⊢ (𝐹:∅–1-1-onto→A ↔
(𝐹 = ∅ ∧ A =
∅)) |