Proof of Theorem brinxper
| Step | Hyp | Ref
| Expression |
| 1 | | relinxp 5824 |
. 2
⊢ Rel (
∼
∩ (𝑉 × 𝑉)) |
| 2 | | brxp 5734 |
. . . . 5
⊢ (𝑥(𝑉 × 𝑉)𝑦 ↔ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) |
| 3 | | brinxper.s |
. . . . . . 7
⊢ (𝑥 ∈ 𝑉 → (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥)) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥)) |
| 5 | | ancom 460 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ↔ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) |
| 6 | | brxp 5734 |
. . . . . . 7
⊢ (𝑦(𝑉 × 𝑉)𝑥 ↔ (𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) |
| 7 | 5, 6 | sylbb2 238 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑦(𝑉 × 𝑉)𝑥) |
| 8 | 4, 7 | jctird 526 |
. . . . 5
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑥 ∧ 𝑦(𝑉 × 𝑉)𝑥))) |
| 9 | 2, 8 | sylbi 217 |
. . . 4
⊢ (𝑥(𝑉 × 𝑉)𝑦 → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑥 ∧ 𝑦(𝑉 × 𝑉)𝑥))) |
| 10 | 9 | impcom 407 |
. . 3
⊢ ((𝑥 ∼ 𝑦 ∧ 𝑥(𝑉 × 𝑉)𝑦) → (𝑦 ∼ 𝑥 ∧ 𝑦(𝑉 × 𝑉)𝑥)) |
| 11 | | brin 5195 |
. . 3
⊢ (𝑥( ∼ ∩ (𝑉 × 𝑉))𝑦 ↔ (𝑥 ∼ 𝑦 ∧ 𝑥(𝑉 × 𝑉)𝑦)) |
| 12 | | brin 5195 |
. . 3
⊢ (𝑦( ∼ ∩ (𝑉 × 𝑉))𝑥 ↔ (𝑦 ∼ 𝑥 ∧ 𝑦(𝑉 × 𝑉)𝑥)) |
| 13 | 10, 11, 12 | 3imtr4i 292 |
. 2
⊢ (𝑥( ∼ ∩ (𝑉 × 𝑉))𝑦 → 𝑦( ∼ ∩ (𝑉 × 𝑉))𝑥) |
| 14 | | brin 5195 |
. . . . . . 7
⊢ (𝑦( ∼ ∩ (𝑉 × 𝑉))𝑧 ↔ (𝑦 ∼ 𝑧 ∧ 𝑦(𝑉 × 𝑉)𝑧)) |
| 15 | | brxp 5734 |
. . . . . . . . . 10
⊢ (𝑦(𝑉 × 𝑉)𝑧 ↔ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) |
| 16 | | brinxper.t |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑉 → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)) |
| 17 | 16 | expd 415 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑉 → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧))) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧))) |
| 19 | 18 | impcom 407 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧)) |
| 20 | 19 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∼ 𝑧 → ((𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∼ 𝑧)) |
| 21 | 20 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ 𝑦 ∼ 𝑧) → ((𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∼ 𝑧)) |
| 22 | 21 | imp 406 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ 𝑦 ∼ 𝑧) ∧ (𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) → 𝑥 ∼ 𝑧) |
| 23 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ 𝑦 ∼ 𝑧) → 𝑧 ∈ 𝑉) |
| 24 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → 𝑥 ∈ 𝑉) |
| 25 | 23, 24 | anim12ci 614 |
. . . . . . . . . . . 12
⊢ ((((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ 𝑦 ∼ 𝑧) ∧ (𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) → (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) |
| 26 | 22, 25 | jca 511 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) ∧ 𝑦 ∼ 𝑧) ∧ (𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) → (𝑥 ∼ 𝑧 ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉))) |
| 27 | 26 | exp31 419 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑦 ∼ 𝑧 → ((𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 ∼ 𝑧 ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉))))) |
| 28 | 15, 27 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑦(𝑉 × 𝑉)𝑧 → (𝑦 ∼ 𝑧 → ((𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 ∼ 𝑧 ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉))))) |
| 29 | 28 | impcom 407 |
. . . . . . . 8
⊢ ((𝑦 ∼ 𝑧 ∧ 𝑦(𝑉 × 𝑉)𝑧) → ((𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 ∼ 𝑧 ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)))) |
| 30 | 2 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝑥 ∼ 𝑦 ∧ 𝑥(𝑉 × 𝑉)𝑦) ↔ (𝑥 ∼ 𝑦 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
| 31 | | brxp 5734 |
. . . . . . . . 9
⊢ (𝑥(𝑉 × 𝑉)𝑧 ↔ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) |
| 32 | 31 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝑥 ∼ 𝑧 ∧ 𝑥(𝑉 × 𝑉)𝑧) ↔ (𝑥 ∼ 𝑧 ∧ (𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉))) |
| 33 | 29, 30, 32 | 3imtr4g 296 |
. . . . . . 7
⊢ ((𝑦 ∼ 𝑧 ∧ 𝑦(𝑉 × 𝑉)𝑧) → ((𝑥 ∼ 𝑦 ∧ 𝑥(𝑉 × 𝑉)𝑦) → (𝑥 ∼ 𝑧 ∧ 𝑥(𝑉 × 𝑉)𝑧))) |
| 34 | 14, 33 | sylbi 217 |
. . . . . 6
⊢ (𝑦( ∼ ∩ (𝑉 × 𝑉))𝑧 → ((𝑥 ∼ 𝑦 ∧ 𝑥(𝑉 × 𝑉)𝑦) → (𝑥 ∼ 𝑧 ∧ 𝑥(𝑉 × 𝑉)𝑧))) |
| 35 | 34 | com12 32 |
. . . . 5
⊢ ((𝑥 ∼ 𝑦 ∧ 𝑥(𝑉 × 𝑉)𝑦) → (𝑦( ∼ ∩ (𝑉 × 𝑉))𝑧 → (𝑥 ∼ 𝑧 ∧ 𝑥(𝑉 × 𝑉)𝑧))) |
| 36 | 11, 35 | sylbi 217 |
. . . 4
⊢ (𝑥( ∼ ∩ (𝑉 × 𝑉))𝑦 → (𝑦( ∼ ∩ (𝑉 × 𝑉))𝑧 → (𝑥 ∼ 𝑧 ∧ 𝑥(𝑉 × 𝑉)𝑧))) |
| 37 | 36 | imp 406 |
. . 3
⊢ ((𝑥( ∼ ∩ (𝑉 × 𝑉))𝑦 ∧ 𝑦( ∼ ∩ (𝑉 × 𝑉))𝑧) → (𝑥 ∼ 𝑧 ∧ 𝑥(𝑉 × 𝑉)𝑧)) |
| 38 | | brin 5195 |
. . 3
⊢ (𝑥( ∼ ∩ (𝑉 × 𝑉))𝑧 ↔ (𝑥 ∼ 𝑧 ∧ 𝑥(𝑉 × 𝑉)𝑧)) |
| 39 | 37, 38 | sylibr 234 |
. 2
⊢ ((𝑥( ∼ ∩ (𝑉 × 𝑉))𝑦 ∧ 𝑦( ∼ ∩ (𝑉 × 𝑉))𝑧) → 𝑥( ∼ ∩ (𝑉 × 𝑉))𝑧) |
| 40 | | brinxper.r |
. . . . 5
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∼ 𝑥) |
| 41 | | id 22 |
. . . . . 6
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑉) |
| 42 | | brxp 5734 |
. . . . . 6
⊢ (𝑥(𝑉 × 𝑉)𝑥 ↔ (𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) |
| 43 | 41, 41, 42 | sylanbrc 583 |
. . . . 5
⊢ (𝑥 ∈ 𝑉 → 𝑥(𝑉 × 𝑉)𝑥) |
| 44 | 40, 43 | jca 511 |
. . . 4
⊢ (𝑥 ∈ 𝑉 → (𝑥 ∼ 𝑥 ∧ 𝑥(𝑉 × 𝑉)𝑥)) |
| 45 | 42 | simplbi 497 |
. . . . 5
⊢ (𝑥(𝑉 × 𝑉)𝑥 → 𝑥 ∈ 𝑉) |
| 46 | 45 | adantl 481 |
. . . 4
⊢ ((𝑥 ∼ 𝑥 ∧ 𝑥(𝑉 × 𝑉)𝑥) → 𝑥 ∈ 𝑉) |
| 47 | 44, 46 | impbii 209 |
. . 3
⊢ (𝑥 ∈ 𝑉 ↔ (𝑥 ∼ 𝑥 ∧ 𝑥(𝑉 × 𝑉)𝑥)) |
| 48 | | brin 5195 |
. . 3
⊢ (𝑥( ∼ ∩ (𝑉 × 𝑉))𝑥 ↔ (𝑥 ∼ 𝑥 ∧ 𝑥(𝑉 × 𝑉)𝑥)) |
| 49 | 47, 48 | bitr4i 278 |
. 2
⊢ (𝑥 ∈ 𝑉 ↔ 𝑥( ∼ ∩ (𝑉 × 𝑉))𝑥) |
| 50 | 1, 13, 39, 49 | iseri 8772 |
1
⊢ ( ∼ ∩
(𝑉 × 𝑉)) Er 𝑉 |