Proof of Theorem dffun2OLDOLD
| Step | Hyp | Ref
| Expression |
| 1 | | df-fun 6563 |
. 2
⊢ (Fun
𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) |
| 2 | | df-id 5578 |
. . . . . 6
⊢ I =
{〈𝑦, 𝑧〉 ∣ 𝑦 = 𝑧} |
| 3 | 2 | sseq2i 4013 |
. . . . 5
⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ (𝐴 ∘ ◡𝐴) ⊆ {〈𝑦, 𝑧〉 ∣ 𝑦 = 𝑧}) |
| 4 | | df-co 5694 |
. . . . . 6
⊢ (𝐴 ∘ ◡𝐴) = {〈𝑦, 𝑧〉 ∣ ∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧)} |
| 5 | 4 | sseq1i 4012 |
. . . . 5
⊢ ((𝐴 ∘ ◡𝐴) ⊆ {〈𝑦, 𝑧〉 ∣ 𝑦 = 𝑧} ↔ {〈𝑦, 𝑧〉 ∣ ∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧)} ⊆ {〈𝑦, 𝑧〉 ∣ 𝑦 = 𝑧}) |
| 6 | | ssopab2bw 5552 |
. . . . 5
⊢
({〈𝑦, 𝑧〉 ∣ ∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧)} ⊆ {〈𝑦, 𝑧〉 ∣ 𝑦 = 𝑧} ↔ ∀𝑦∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 7 | 3, 5, 6 | 3bitri 297 |
. . . 4
⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑦∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 8 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
| 9 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 10 | 8, 9 | brcnv 5893 |
. . . . . . . . . . 11
⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦) |
| 11 | 10 | anbi1i 624 |
. . . . . . . . . 10
⊢ ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧)) |
| 12 | 11 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ ∃𝑥(𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧)) |
| 13 | 12 | imbi1i 349 |
. . . . . . . 8
⊢
((∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ (∃𝑥(𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 14 | | 19.23v 1942 |
. . . . . . . 8
⊢
(∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ (∃𝑥(𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 15 | 13, 14 | bitr4i 278 |
. . . . . . 7
⊢
((∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 16 | 15 | albii 1819 |
. . . . . 6
⊢
(∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑧∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 17 | | alcom 2159 |
. . . . . 6
⊢
(∀𝑧∀𝑥((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 18 | 16, 17 | bitri 275 |
. . . . 5
⊢
(∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 19 | 18 | albii 1819 |
. . . 4
⊢
(∀𝑦∀𝑧(∃𝑥(𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑦∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 20 | | alcom 2159 |
. . . 4
⊢
(∀𝑦∀𝑥∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 21 | 7, 19, 20 | 3bitri 297 |
. . 3
⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) |
| 22 | 21 | anbi2i 623 |
. 2
⊢ ((Rel
𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ) ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) |
| 23 | 1, 22 | bitri 275 |
1
⊢ (Fun
𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) |