| Step | Hyp | Ref
| Expression |
| 1 | | fcoinvbr.e |
. . . . 5
⊢ ∼ =
(◡𝐹 ∘ 𝐹) |
| 2 | 1 | breqi 5149 |
. . . 4
⊢ (𝑋 ∼ 𝑌 ↔ 𝑋(◡𝐹 ∘ 𝐹)𝑌) |
| 3 | | brcog 5877 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋(◡𝐹 ∘ 𝐹)𝑌 ↔ ∃𝑧(𝑋𝐹𝑧 ∧ 𝑧◡𝐹𝑌))) |
| 4 | 2, 3 | bitrid 283 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∼ 𝑌 ↔ ∃𝑧(𝑋𝐹𝑧 ∧ 𝑧◡𝐹𝑌))) |
| 5 | 4 | 3adant1 1131 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∼ 𝑌 ↔ ∃𝑧(𝑋𝐹𝑧 ∧ 𝑧◡𝐹𝑌))) |
| 6 | | fvex 6919 |
. . . . 5
⊢ (𝐹‘𝑋) ∈ V |
| 7 | 6 | eqvinc 3649 |
. . . 4
⊢ ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ ∃𝑧(𝑧 = (𝐹‘𝑋) ∧ 𝑧 = (𝐹‘𝑌))) |
| 8 | | eqcom 2744 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = 𝑧) |
| 9 | | eqcom 2744 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝑌) ↔ (𝐹‘𝑌) = 𝑧) |
| 10 | 8, 9 | anbi12i 628 |
. . . . 5
⊢ ((𝑧 = (𝐹‘𝑋) ∧ 𝑧 = (𝐹‘𝑌)) ↔ ((𝐹‘𝑋) = 𝑧 ∧ (𝐹‘𝑌) = 𝑧)) |
| 11 | 10 | exbii 1848 |
. . . 4
⊢
(∃𝑧(𝑧 = (𝐹‘𝑋) ∧ 𝑧 = (𝐹‘𝑌)) ↔ ∃𝑧((𝐹‘𝑋) = 𝑧 ∧ (𝐹‘𝑌) = 𝑧)) |
| 12 | 7, 11 | bitri 275 |
. . 3
⊢ ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ ∃𝑧((𝐹‘𝑋) = 𝑧 ∧ (𝐹‘𝑌) = 𝑧)) |
| 13 | | fnbrfvb 6959 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑧 ↔ 𝑋𝐹𝑧)) |
| 14 | 13 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑧 ↔ 𝑋𝐹𝑧)) |
| 15 | | fnbrfvb 6959 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑌) = 𝑧 ↔ 𝑌𝐹𝑧)) |
| 16 | 15 | 3adant2 1132 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑌) = 𝑧 ↔ 𝑌𝐹𝑧)) |
| 17 | 14, 16 | anbi12d 632 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (((𝐹‘𝑋) = 𝑧 ∧ (𝐹‘𝑌) = 𝑧) ↔ (𝑋𝐹𝑧 ∧ 𝑌𝐹𝑧))) |
| 18 | | vex 3484 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
| 19 | | brcnvg 5890 |
. . . . . . . 8
⊢ ((𝑧 ∈ V ∧ 𝑌 ∈ 𝐴) → (𝑧◡𝐹𝑌 ↔ 𝑌𝐹𝑧)) |
| 20 | 18, 19 | mpan 690 |
. . . . . . 7
⊢ (𝑌 ∈ 𝐴 → (𝑧◡𝐹𝑌 ↔ 𝑌𝐹𝑧)) |
| 21 | 20 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑧◡𝐹𝑌 ↔ 𝑌𝐹𝑧)) |
| 22 | 21 | anbi2d 630 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝑋𝐹𝑧 ∧ 𝑧◡𝐹𝑌) ↔ (𝑋𝐹𝑧 ∧ 𝑌𝐹𝑧))) |
| 23 | 17, 22 | bitr4d 282 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (((𝐹‘𝑋) = 𝑧 ∧ (𝐹‘𝑌) = 𝑧) ↔ (𝑋𝐹𝑧 ∧ 𝑧◡𝐹𝑌))) |
| 24 | 23 | exbidv 1921 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∃𝑧((𝐹‘𝑋) = 𝑧 ∧ (𝐹‘𝑌) = 𝑧) ↔ ∃𝑧(𝑋𝐹𝑧 ∧ 𝑧◡𝐹𝑌))) |
| 25 | 12, 24 | bitrid 283 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ ∃𝑧(𝑋𝐹𝑧 ∧ 𝑧◡𝐹𝑌))) |
| 26 | 5, 25 | bitr4d 282 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌))) |