Proof of Theorem fsneqrn
Step | Hyp | Ref
| Expression |
1 | | fsneqrn.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐵) |
2 | | dffn3 6613 |
. . . . . . 7
⊢ (𝐹 Fn 𝐵 ↔ 𝐹:𝐵⟶ran 𝐹) |
3 | 1, 2 | sylib 217 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐵⟶ran 𝐹) |
4 | | fsneqrn.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | snidg 4595 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
7 | | fsneqrn.b |
. . . . . . . . 9
⊢ 𝐵 = {𝐴} |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = {𝐴}) |
9 | 8 | eqcomd 2744 |
. . . . . . 7
⊢ (𝜑 → {𝐴} = 𝐵) |
10 | 6, 9 | eleqtrd 2841 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
11 | 3, 10 | ffvelrnd 6962 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝐴) ∈ ran 𝐹) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → (𝐹‘𝐴) ∈ ran 𝐹) |
13 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → 𝐹 = 𝐺) |
14 | 13 | rneqd 5847 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → ran 𝐹 = ran 𝐺) |
15 | 12, 14 | eleqtrd 2841 |
. . 3
⊢ ((𝜑 ∧ 𝐹 = 𝐺) → (𝐹‘𝐴) ∈ ran 𝐺) |
16 | 15 | ex 413 |
. 2
⊢ (𝜑 → (𝐹 = 𝐺 → (𝐹‘𝐴) ∈ ran 𝐺)) |
17 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹‘𝐴) ∈ ran 𝐺) |
18 | | fsneqrn.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 Fn 𝐵) |
19 | | dffn2 6602 |
. . . . . . . . . 10
⊢ (𝐺 Fn 𝐵 ↔ 𝐺:𝐵⟶V) |
20 | 18, 19 | sylib 217 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐵⟶V) |
21 | 8 | feq2d 6586 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺:𝐵⟶V ↔ 𝐺:{𝐴}⟶V)) |
22 | 20, 21 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:{𝐴}⟶V) |
23 | 4, 22 | rnsnf 42721 |
. . . . . . 7
⊢ (𝜑 → ran 𝐺 = {(𝐺‘𝐴)}) |
24 | 23 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → ran 𝐺 = {(𝐺‘𝐴)}) |
25 | 17, 24 | eleqtrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹‘𝐴) ∈ {(𝐺‘𝐴)}) |
26 | | elsni 4578 |
. . . . 5
⊢ ((𝐹‘𝐴) ∈ {(𝐺‘𝐴)} → (𝐹‘𝐴) = (𝐺‘𝐴)) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹‘𝐴) = (𝐺‘𝐴)) |
28 | 4 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐴 ∈ 𝑉) |
29 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐹 Fn 𝐵) |
30 | 18 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐺 Fn 𝐵) |
31 | 28, 7, 29, 30 | fsneq 42746 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴))) |
32 | 27, 31 | mpbird 256 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐴) ∈ ran 𝐺) → 𝐹 = 𝐺) |
33 | 32 | ex 413 |
. 2
⊢ (𝜑 → ((𝐹‘𝐴) ∈ ran 𝐺 → 𝐹 = 𝐺)) |
34 | 16, 33 | impbid 211 |
1
⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺)) |