Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . 3
⊢ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ 𝑅 |
2 | | psrel 17203 |
. . 3
⊢ (𝑅 ∈ PosetRel → Rel
𝑅) |
3 | | relss 5206 |
. . 3
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ⊆ 𝑅 → (Rel 𝑅 → Rel (𝑅 ∩ (𝐴 × 𝐴)))) |
4 | 1, 2, 3 | mpsyl 68 |
. 2
⊢ (𝑅 ∈ PosetRel → Rel
(𝑅 ∩ (𝐴 × 𝐴))) |
5 | | pstr2 17205 |
. . 3
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅) |
6 | | trinxp 5521 |
. . 3
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) |
7 | 5, 6 | syl 17 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) |
8 | | uniin 4457 |
. . . . . 6
⊢ ∪ (𝑅
∩ (𝐴 × 𝐴)) ⊆ (∪ 𝑅
∩ ∪ (𝐴 × 𝐴)) |
9 | 8 | unissi 4461 |
. . . . 5
⊢ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ ∪
(∪ 𝑅 ∩ ∪ (𝐴 × 𝐴)) |
10 | | uniin 4457 |
. . . . 5
⊢ ∪ (∪ 𝑅 ∩ ∪ (𝐴 × 𝐴)) ⊆ (∪
∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) |
11 | 9, 10 | sstri 3612 |
. . . 4
⊢ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ (∪
∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) |
12 | | elin 3796 |
. . . . . 6
⊢ (𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) ↔ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ ∪ ∪ (𝐴
× 𝐴))) |
13 | | unixpid 5670 |
. . . . . . . . 9
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴 |
14 | 13 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ ∪ (𝐴 × 𝐴) ↔ 𝑥 ∈ 𝐴) |
15 | | simprr 796 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ PosetRel ∧ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
16 | | psdmrn 17207 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ PosetRel → (dom
𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅)) |
17 | 16 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ PosetRel → dom
𝑅 = ∪ ∪ 𝑅) |
18 | 17 | eleq2d 2687 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ PosetRel → (𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ ∪ ∪ 𝑅)) |
19 | 18 | biimpar 502 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → 𝑥 ∈ dom 𝑅) |
20 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ dom 𝑅 = dom 𝑅 |
21 | 20 | psref 17208 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → 𝑥𝑅𝑥) |
22 | 19, 21 | syldan 487 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → 𝑥𝑅𝑥) |
23 | 22 | adantrr 753 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ PosetRel ∧ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴)) → 𝑥𝑅𝑥) |
24 | | brinxp2 5180 |
. . . . . . . . . 10
⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥𝑅𝑥)) |
25 | 15, 15, 23, 24 | syl3anbrc 1246 |
. . . . . . . . 9
⊢ ((𝑅 ∈ PosetRel ∧ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴)) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥) |
26 | 25 | expr 643 |
. . . . . . . 8
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → (𝑥 ∈ 𝐴 → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
27 | 14, 26 | syl5bi 232 |
. . . . . . 7
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → (𝑥 ∈ ∪ ∪ (𝐴
× 𝐴) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
28 | 27 | expimpd 629 |
. . . . . 6
⊢ (𝑅 ∈ PosetRel → ((𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ ∪ ∪ (𝐴
× 𝐴)) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
29 | 12, 28 | syl5bi 232 |
. . . . 5
⊢ (𝑅 ∈ PosetRel → (𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
30 | 29 | ralrimiv 2965 |
. . . 4
⊢ (𝑅 ∈ PosetRel →
∀𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥) |
31 | | ssralv 3666 |
. . . 4
⊢ (∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ (∪
∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) →
(∀𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥 → ∀𝑥 ∈ ∪ ∪ (𝑅
∩ (𝐴 × 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
32 | 11, 30, 31 | mpsyl 68 |
. . 3
⊢ (𝑅 ∈ PosetRel →
∀𝑥 ∈ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥) |
33 | 1 | ssbri 4697 |
. . . . 5
⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 → 𝑥𝑅𝑦) |
34 | 1 | ssbri 4697 |
. . . . 5
⊢ (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥 → 𝑦𝑅𝑥) |
35 | | psasym 17210 |
. . . . . 6
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) |
36 | 35 | 3expib 1268 |
. . . . 5
⊢ (𝑅 ∈ PosetRel → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
37 | 33, 34, 36 | syl2ani 688 |
. . . 4
⊢ (𝑅 ∈ PosetRel → ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥) → 𝑥 = 𝑦)) |
38 | 37 | alrimivv 1856 |
. . 3
⊢ (𝑅 ∈ PosetRel →
∀𝑥∀𝑦((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥) → 𝑥 = 𝑦)) |
39 | | asymref2 5513 |
. . 3
⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑥 ∈ ∪ ∪ (𝑅
∩ (𝐴 × 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥 ∧ ∀𝑥∀𝑦((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥) → 𝑥 = 𝑦))) |
40 | 32, 38, 39 | sylanbrc 698 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)))) |
41 | | inex1g 4801 |
. . 3
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) |
42 | | isps 17202 |
. . 3
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel ↔ (Rel (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)))))) |
43 | 41, 42 | syl 17 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel ↔ (Rel (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)))))) |
44 | 4, 7, 40, 43 | mpbir3and 1245 |
1
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) |