Step | Hyp | Ref
| Expression |
1 | | inss1 4167 |
. . 3
⊢ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ 𝑅 |
2 | | psrel 18268 |
. . 3
⊢ (𝑅 ∈ PosetRel → Rel
𝑅) |
3 | | relss 5690 |
. . 3
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ⊆ 𝑅 → (Rel 𝑅 → Rel (𝑅 ∩ (𝐴 × 𝐴)))) |
4 | 1, 2, 3 | mpsyl 68 |
. 2
⊢ (𝑅 ∈ PosetRel → Rel
(𝑅 ∩ (𝐴 × 𝐴))) |
5 | | pstr2 18270 |
. . 3
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅) |
6 | | trinxp 6027 |
. . 3
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) |
7 | 5, 6 | syl 17 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) |
8 | | uniin 4870 |
. . . . . 6
⊢ ∪ (𝑅
∩ (𝐴 × 𝐴)) ⊆ (∪ 𝑅
∩ ∪ (𝐴 × 𝐴)) |
9 | 8 | unissi 4853 |
. . . . 5
⊢ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ ∪
(∪ 𝑅 ∩ ∪ (𝐴 × 𝐴)) |
10 | | uniin 4870 |
. . . . 5
⊢ ∪ (∪ 𝑅 ∩ ∪ (𝐴 × 𝐴)) ⊆ (∪
∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) |
11 | 9, 10 | sstri 3934 |
. . . 4
⊢ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ (∪
∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) |
12 | | elin 3907 |
. . . . . 6
⊢ (𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) ↔ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ ∪ ∪ (𝐴
× 𝐴))) |
13 | | unixpid 6184 |
. . . . . . . . 9
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴 |
14 | 13 | eleq2i 2831 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ ∪ (𝐴 × 𝐴) ↔ 𝑥 ∈ 𝐴) |
15 | | simprr 769 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ PosetRel ∧ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
16 | | psdmrn 18272 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ PosetRel → (dom
𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅)) |
17 | 16 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ PosetRel → dom
𝑅 = ∪ ∪ 𝑅) |
18 | 17 | eleq2d 2825 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ PosetRel → (𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ ∪ ∪ 𝑅)) |
19 | 18 | biimpar 477 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → 𝑥 ∈ dom 𝑅) |
20 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢ dom 𝑅 = dom 𝑅 |
21 | 20 | psref 18273 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅) → 𝑥𝑅𝑥) |
22 | 19, 21 | syldan 590 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → 𝑥𝑅𝑥) |
23 | 22 | adantrr 713 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ PosetRel ∧ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴)) → 𝑥𝑅𝑥) |
24 | | brinxp2 5663 |
. . . . . . . . . 10
⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥𝑅𝑥)) |
25 | 15, 15, 23, 24 | syl21anbrc 1342 |
. . . . . . . . 9
⊢ ((𝑅 ∈ PosetRel ∧ (𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴)) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥) |
26 | 25 | expr 456 |
. . . . . . . 8
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → (𝑥 ∈ 𝐴 → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
27 | 14, 26 | syl5bi 241 |
. . . . . . 7
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅) → (𝑥 ∈ ∪ ∪ (𝐴
× 𝐴) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
28 | 27 | expimpd 453 |
. . . . . 6
⊢ (𝑅 ∈ PosetRel → ((𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ ∪ ∪ (𝐴
× 𝐴)) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
29 | 12, 28 | syl5bi 241 |
. . . . 5
⊢ (𝑅 ∈ PosetRel → (𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) → 𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
30 | 29 | ralrimiv 3108 |
. . . 4
⊢ (𝑅 ∈ PosetRel →
∀𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥) |
31 | | ssralv 3991 |
. . . 4
⊢ (∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)) ⊆ (∪
∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴)) →
(∀𝑥 ∈ (∪ ∪ 𝑅 ∩ ∪ ∪ (𝐴
× 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥 → ∀𝑥 ∈ ∪ ∪ (𝑅
∩ (𝐴 × 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
32 | 11, 30, 31 | mpsyl 68 |
. . 3
⊢ (𝑅 ∈ PosetRel →
∀𝑥 ∈ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥) |
33 | 1 | ssbri 5123 |
. . . . 5
⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 → 𝑥𝑅𝑦) |
34 | 1 | ssbri 5123 |
. . . . 5
⊢ (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥 → 𝑦𝑅𝑥) |
35 | | psasym 18275 |
. . . . . 6
⊢ ((𝑅 ∈ PosetRel ∧ 𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦) |
36 | 35 | 3expib 1120 |
. . . . 5
⊢ (𝑅 ∈ PosetRel → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) |
37 | 33, 34, 36 | syl2ani 606 |
. . . 4
⊢ (𝑅 ∈ PosetRel → ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥) → 𝑥 = 𝑦)) |
38 | 37 | alrimivv 1934 |
. . 3
⊢ (𝑅 ∈ PosetRel →
∀𝑥∀𝑦((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥) → 𝑥 = 𝑦)) |
39 | | asymref2 6019 |
. . 3
⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑥 ∈ ∪ ∪ (𝑅
∩ (𝐴 × 𝐴))𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑥 ∧ ∀𝑥∀𝑦((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥) → 𝑥 = 𝑦))) |
40 | 32, 38, 39 | sylanbrc 582 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)))) |
41 | | inex1g 5246 |
. . 3
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) |
42 | | isps 18267 |
. . 3
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel ↔ (Rel (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)))))) |
43 | 41, 42 | syl 17 |
. 2
⊢ (𝑅 ∈ PosetRel → ((𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel ↔ (Rel (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴)) ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∩ ◡(𝑅 ∩ (𝐴 × 𝐴))) = ( I ↾ ∪ ∪ (𝑅 ∩ (𝐴 × 𝐴)))))) |
44 | 4, 7, 40, 43 | mpbir3and 1340 |
1
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) |