Step | Hyp | Ref
| Expression |
1 | | sseq1 3180 |
. . 3
⊢ (𝑅 = 𝑆 → (𝑅 ⊆ (𝐴 × 𝐴) ↔ 𝑆 ⊆ (𝐴 × 𝐴))) |
2 | | breq 4007 |
. . . . . 6
⊢ (𝑅 = 𝑆 → (𝑥𝑅𝑥 ↔ 𝑥𝑆𝑥)) |
3 | 2 | notbid 667 |
. . . . 5
⊢ (𝑅 = 𝑆 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑥𝑆𝑥)) |
4 | 3 | ralbidv 2477 |
. . . 4
⊢ (𝑅 = 𝑆 → (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑆𝑥)) |
5 | | breq 4007 |
. . . . . 6
⊢ (𝑅 = 𝑆 → (𝑥𝑅𝑦 ↔ 𝑥𝑆𝑦)) |
6 | | breq 4007 |
. . . . . 6
⊢ (𝑅 = 𝑆 → (𝑦𝑅𝑥 ↔ 𝑦𝑆𝑥)) |
7 | 5, 6 | imbi12d 234 |
. . . . 5
⊢ (𝑅 = 𝑆 → ((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ (𝑥𝑆𝑦 → 𝑦𝑆𝑥))) |
8 | 7 | 2ralbidv 2501 |
. . . 4
⊢ (𝑅 = 𝑆 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑆𝑦 → 𝑦𝑆𝑥))) |
9 | 4, 8 | anbi12d 473 |
. . 3
⊢ (𝑅 = 𝑆 → ((∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑆𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑆𝑦 → 𝑦𝑆𝑥)))) |
10 | | breq 4007 |
. . . . . . . 8
⊢ (𝑅 = 𝑆 → (𝑥𝑅𝑧 ↔ 𝑥𝑆𝑧)) |
11 | | breq 4007 |
. . . . . . . 8
⊢ (𝑅 = 𝑆 → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) |
12 | 10, 11 | orbi12d 793 |
. . . . . . 7
⊢ (𝑅 = 𝑆 → ((𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧) ↔ (𝑥𝑆𝑧 ∨ 𝑦𝑆𝑧))) |
13 | 5, 12 | imbi12d 234 |
. . . . . 6
⊢ (𝑅 = 𝑆 → ((𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ↔ (𝑥𝑆𝑦 → (𝑥𝑆𝑧 ∨ 𝑦𝑆𝑧)))) |
14 | 13 | ralbidv 2477 |
. . . . 5
⊢ (𝑅 = 𝑆 → (∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ↔ ∀𝑧 ∈ 𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧 ∨ 𝑦𝑆𝑧)))) |
15 | 14 | 2ralbidv 2501 |
. . . 4
⊢ (𝑅 = 𝑆 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧 ∨ 𝑦𝑆𝑧)))) |
16 | 5 | notbid 667 |
. . . . . 6
⊢ (𝑅 = 𝑆 → (¬ 𝑥𝑅𝑦 ↔ ¬ 𝑥𝑆𝑦)) |
17 | 16 | imbi1d 231 |
. . . . 5
⊢ (𝑅 = 𝑆 → ((¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦) ↔ (¬ 𝑥𝑆𝑦 → 𝑥 = 𝑦))) |
18 | 17 | 2ralbidv 2501 |
. . . 4
⊢ (𝑅 = 𝑆 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑆𝑦 → 𝑥 = 𝑦))) |
19 | 15, 18 | anbi12d 473 |
. . 3
⊢ (𝑅 = 𝑆 → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧 ∨ 𝑦𝑆𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑆𝑦 → 𝑥 = 𝑦)))) |
20 | 1, 9, 19 | 3anbi123d 1312 |
. 2
⊢ (𝑅 = 𝑆 → ((𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦))) ↔ (𝑆 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑆𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑆𝑦 → 𝑦𝑆𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧 ∨ 𝑦𝑆𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑆𝑦 → 𝑥 = 𝑦))))) |
21 | | dftap2 7252 |
. 2
⊢ (𝑅 TAp 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)))) |
22 | | dftap2 7252 |
. 2
⊢ (𝑆 TAp 𝐴 ↔ (𝑆 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑆𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑆𝑦 → 𝑦𝑆𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑆𝑦 → (𝑥𝑆𝑧 ∨ 𝑦𝑆𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑆𝑦 → 𝑥 = 𝑦)))) |
23 | 20, 21, 22 | 3bitr4g 223 |
1
⊢ (𝑅 = 𝑆 → (𝑅 TAp 𝐴 ↔ 𝑆 TAp 𝐴)) |