Proof of Theorem fsneqrn
| Step | Hyp | Ref
| Expression |
| 1 | | fsneqrn.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐵) |
| 2 | | dffn3 6748 |
. . . . . . 7
⊢ (𝐹 Fn 𝐵 ↔ 𝐹:𝐵⟶ran 𝐹) |
| 3 | 1, 2 | sylib 218 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐵⟶ran 𝐹) |
| 4 | | fsneqrn.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 5 | | snidg 4660 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
| 6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
| 7 | | fsneqrn.b |
. . . . . . . . 9
⊢ 𝐵 = {𝐴} |
| 8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = {𝐴}) |
| 9 | 8 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → {𝐴} = 𝐵) |
| 10 | 6, 9 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
| 11 | 3, 10 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) ∈ ran 𝐹) |
| 12 | 11 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → (𝐹‘𝐴) ∈ ran 𝐹) |
| 13 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → 𝐹 = 𝐺) |
| 14 | 13 | rneqd 5949 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → ran 𝐹 = ran 𝐺) |
| 15 | 12, 14 | eleqtrd 2843 |
. . 3
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → (𝐹‘𝐴) ∈ ran 𝐺) |
| 16 | 15 | ex 412 |
. 2
⊢ (𝜑 → (𝐹 = 𝐺 → (𝐹‘𝐴) ∈ ran 𝐺)) |
| 17 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹‘𝐴) ∈ ran 𝐺) |
| 18 | | fsneqrn.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 Fn 𝐵) |
| 19 | | dffn2 6738 |
. . . . . . . . . 10
⊢ (𝐺 Fn 𝐵 ↔ 𝐺:𝐵⟶V) |
| 20 | 18, 19 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐵⟶V) |
| 21 | 8 | feq2d 6722 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺:𝐵⟶V ↔ 𝐺:{𝐴}⟶V)) |
| 22 | 20, 21 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:{𝐴}⟶V) |
| 23 | 4, 22 | rnsnf 45189 |
. . . . . . 7
⊢ (𝜑 → ran 𝐺 = {(𝐺‘𝐴)}) |
| 24 | 23 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → ran 𝐺 = {(𝐺‘𝐴)}) |
| 25 | 17, 24 | eleqtrd 2843 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹‘𝐴) ∈ {(𝐺‘𝐴)}) |
| 26 | | elsni 4643 |
. . . . 5
⊢ ((𝐹‘𝐴) ∈ {(𝐺‘𝐴)} → (𝐹‘𝐴) = (𝐺‘𝐴)) |
| 27 | 25, 26 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴)) |
| 28 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐴 ∈ 𝑉) |
| 29 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐹 Fn 𝐵) |
| 30 | 18 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐺 Fn 𝐵) |
| 31 | 28, 7, 29, 30 | fsneq 45211 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴))) |
| 32 | 27, 31 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐹 = 𝐺) |
| 33 | 32 | ex 412 |
. 2
⊢ (𝜑 → ((𝐹‘𝐴) ∈ ran 𝐺 → 𝐹 = 𝐺)) |
| 34 | 16, 33 | impbid 212 |
1
⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺)) |