Step | Hyp | Ref
| Expression |
1 | | inss2 3796 |
. . . 4
⊢ (𝑅 ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
2 | | relxp 5150 |
. . . 4
⊢ Rel
(𝐵 × 𝐵) |
3 | | relss 5129 |
. . . 4
⊢ ((𝑅 ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) → (Rel (𝐵 × 𝐵) → Rel (𝑅 ∩ (𝐵 × 𝐵)))) |
4 | 1, 2, 3 | mp2 9 |
. . 3
⊢ Rel
(𝑅 ∩ (𝐵 × 𝐵)) |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → Rel (𝑅 ∩ (𝐵 × 𝐵))) |
6 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) |
7 | | brinxp2 5103 |
. . . . 5
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥𝑅𝑦)) |
8 | 6, 7 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥𝑅𝑦)) |
9 | 8 | simp2d 1067 |
. . 3
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑦 ∈ 𝐵) |
10 | 8 | simp1d 1066 |
. . 3
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑥 ∈ 𝐵) |
11 | | erinxp.r |
. . . . 5
⊢ (𝜑 → 𝑅 Er 𝐴) |
12 | 11 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑅 Er 𝐴) |
13 | 8 | simp3d 1068 |
. . . 4
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑥𝑅𝑦) |
14 | 12, 13 | ersym 7641 |
. . 3
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑦𝑅𝑥) |
15 | | brinxp2 5103 |
. . 3
⊢ (𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑥 ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) |
16 | 9, 10, 14, 15 | syl3anbrc 1239 |
. 2
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑥) |
17 | 10 | adantrr 749 |
. . 3
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥 ∈ 𝐵) |
18 | | simprr 792 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧) |
19 | | brinxp2 5103 |
. . . . 5
⊢ (𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑦𝑅𝑧)) |
20 | 18, 19 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑦𝑅𝑧)) |
21 | 20 | simp2d 1067 |
. . 3
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑧 ∈ 𝐵) |
22 | 11 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑅 Er 𝐴) |
23 | 13 | adantrr 749 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥𝑅𝑦) |
24 | 20 | simp3d 1068 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑦𝑅𝑧) |
25 | 22, 23, 24 | ertrd 7645 |
. . 3
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥𝑅𝑧) |
26 | | brinxp2 5103 |
. . 3
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑧 ↔ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥𝑅𝑧)) |
27 | 17, 21, 25, 26 | syl3anbrc 1239 |
. 2
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑧) |
28 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 Er 𝐴) |
29 | | erinxp.a |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
30 | 29 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
31 | 28, 30 | erref 7649 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥𝑅𝑥) |
32 | 31 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥𝑅𝑥)) |
33 | 32 | pm4.71rd 665 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ (𝑥𝑅𝑥 ∧ 𝑥 ∈ 𝐵))) |
34 | | brin 4634 |
. . . 4
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑥 ↔ (𝑥𝑅𝑥 ∧ 𝑥(𝐵 × 𝐵)𝑥)) |
35 | | brxp 5071 |
. . . . . 6
⊢ (𝑥(𝐵 × 𝐵)𝑥 ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) |
36 | | anidm 674 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵) |
37 | 35, 36 | bitri 263 |
. . . . 5
⊢ (𝑥(𝐵 × 𝐵)𝑥 ↔ 𝑥 ∈ 𝐵) |
38 | 37 | anbi2i 726 |
. . . 4
⊢ ((𝑥𝑅𝑥 ∧ 𝑥(𝐵 × 𝐵)𝑥) ↔ (𝑥𝑅𝑥 ∧ 𝑥 ∈ 𝐵)) |
39 | 34, 38 | bitri 263 |
. . 3
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑥 ↔ (𝑥𝑅𝑥 ∧ 𝑥 ∈ 𝐵)) |
40 | 33, 39 | syl6bbr 277 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑥)) |
41 | 5, 16, 27, 40 | iserd 7655 |
1
⊢ (𝜑 → (𝑅 ∩ (𝐵 × 𝐵)) Er 𝐵) |