Step | Hyp | Ref
| Expression |
1 | | inss2 3328 |
. . . 4
⊢ (𝑅 ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) |
2 | | relxp 4695 |
. . . 4
⊢ Rel
(𝐵 × 𝐵) |
3 | | relss 4673 |
. . . 4
⊢ ((𝑅 ∩ (𝐵 × 𝐵)) ⊆ (𝐵 × 𝐵) → (Rel (𝐵 × 𝐵) → Rel (𝑅 ∩ (𝐵 × 𝐵)))) |
4 | 1, 2, 3 | mp2 16 |
. . 3
⊢ Rel
(𝑅 ∩ (𝐵 × 𝐵)) |
5 | 4 | a1i 9 |
. 2
⊢ (𝜑 → Rel (𝑅 ∩ (𝐵 × 𝐵))) |
6 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) |
7 | | brinxp2 4653 |
. . . . 5
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥𝑅𝑦)) |
8 | 6, 7 | sylib 121 |
. . . 4
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥𝑅𝑦)) |
9 | 8 | simp2d 995 |
. . 3
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑦 ∈ 𝐵) |
10 | 8 | simp1d 994 |
. . 3
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑥 ∈ 𝐵) |
11 | | erinxp.r |
. . . . 5
⊢ (𝜑 → 𝑅 Er 𝐴) |
12 | 11 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑅 Er 𝐴) |
13 | 8 | simp3d 996 |
. . . 4
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑥𝑅𝑦) |
14 | 12, 13 | ersym 6492 |
. . 3
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑦𝑅𝑥) |
15 | | brinxp2 4653 |
. . 3
⊢ (𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑥 ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦𝑅𝑥)) |
16 | 9, 10, 14, 15 | syl3anbrc 1166 |
. 2
⊢ ((𝜑 ∧ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦) → 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑥) |
17 | 10 | adantrr 471 |
. . 3
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥 ∈ 𝐵) |
18 | | simprr 522 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧) |
19 | | brinxp2 4653 |
. . . . 5
⊢ (𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑦𝑅𝑧)) |
20 | 18, 19 | sylib 121 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑦𝑅𝑧)) |
21 | 20 | simp2d 995 |
. . 3
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑧 ∈ 𝐵) |
22 | 11 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑅 Er 𝐴) |
23 | 13 | adantrr 471 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥𝑅𝑦) |
24 | 20 | simp3d 996 |
. . . 4
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑦𝑅𝑧) |
25 | 22, 23, 24 | ertrd 6496 |
. . 3
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥𝑅𝑧) |
26 | | brinxp2 4653 |
. . 3
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑧 ↔ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥𝑅𝑧)) |
27 | 17, 21, 25, 26 | syl3anbrc 1166 |
. 2
⊢ ((𝜑 ∧ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑦 ∧ 𝑦(𝑅 ∩ (𝐵 × 𝐵))𝑧)) → 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑧) |
28 | 11 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑅 Er 𝐴) |
29 | | erinxp.a |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
30 | 29 | sselda 3128 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
31 | 28, 30 | erref 6500 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥𝑅𝑥) |
32 | 31 | ex 114 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥𝑅𝑥)) |
33 | 32 | pm4.71rd 392 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ (𝑥𝑅𝑥 ∧ 𝑥 ∈ 𝐵))) |
34 | | brin 4016 |
. . . 4
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑥 ↔ (𝑥𝑅𝑥 ∧ 𝑥(𝐵 × 𝐵)𝑥)) |
35 | | brxp 4617 |
. . . . . 6
⊢ (𝑥(𝐵 × 𝐵)𝑥 ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) |
36 | | anidm 394 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵) |
37 | 35, 36 | bitri 183 |
. . . . 5
⊢ (𝑥(𝐵 × 𝐵)𝑥 ↔ 𝑥 ∈ 𝐵) |
38 | 37 | anbi2i 453 |
. . . 4
⊢ ((𝑥𝑅𝑥 ∧ 𝑥(𝐵 × 𝐵)𝑥) ↔ (𝑥𝑅𝑥 ∧ 𝑥 ∈ 𝐵)) |
39 | 34, 38 | bitri 183 |
. . 3
⊢ (𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑥 ↔ (𝑥𝑅𝑥 ∧ 𝑥 ∈ 𝐵)) |
40 | 33, 39 | bitr4di 197 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥(𝑅 ∩ (𝐵 × 𝐵))𝑥)) |
41 | 5, 16, 27, 40 | iserd 6506 |
1
⊢ (𝜑 → (𝑅 ∩ (𝐵 × 𝐵)) Er 𝐵) |