Step |
Hyp |
Ref |
Expression |
1 |
|
inss1 |
⊢ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑅 |
2 |
|
psrel |
⊢ ( 𝑅 ∈ PosetRel → Rel 𝑅 ) |
3 |
|
relss |
⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑅 → ( Rel 𝑅 → Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
4 |
1 2 3
|
mpsyl |
⊢ ( 𝑅 ∈ PosetRel → Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) |
5 |
|
pstr2 |
⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) |
6 |
|
trinxp |
⊢ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) |
7 |
5 6
|
syl |
⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) |
8 |
|
uniin |
⊢ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( ∪ 𝑅 ∩ ∪ ( 𝐴 × 𝐴 ) ) |
9 |
8
|
unissi |
⊢ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ∪ ( ∪ 𝑅 ∩ ∪ ( 𝐴 × 𝐴 ) ) |
10 |
|
uniin |
⊢ ∪ ( ∪ 𝑅 ∩ ∪ ( 𝐴 × 𝐴 ) ) ⊆ ( ∪ ∪ 𝑅 ∩ ∪ ∪ ( 𝐴 × 𝐴 ) ) |
11 |
9 10
|
sstri |
⊢ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( ∪ ∪ 𝑅 ∩ ∪ ∪ ( 𝐴 × 𝐴 ) ) |
12 |
|
elin |
⊢ ( 𝑥 ∈ ( ∪ ∪ 𝑅 ∩ ∪ ∪ ( 𝐴 × 𝐴 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ ∪ ∪ ( 𝐴 × 𝐴 ) ) ) |
13 |
|
unixpid |
⊢ ∪ ∪ ( 𝐴 × 𝐴 ) = 𝐴 |
14 |
13
|
eleq2i |
⊢ ( 𝑥 ∈ ∪ ∪ ( 𝐴 × 𝐴 ) ↔ 𝑥 ∈ 𝐴 ) |
15 |
|
simprr |
⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 ) |
16 |
|
psdmrn |
⊢ ( 𝑅 ∈ PosetRel → ( dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅 ) ) |
17 |
16
|
simpld |
⊢ ( 𝑅 ∈ PosetRel → dom 𝑅 = ∪ ∪ 𝑅 ) |
18 |
17
|
eleq2d |
⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ ∪ ∪ 𝑅 ) ) |
19 |
18
|
biimpar |
⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅 ) → 𝑥 ∈ dom 𝑅 ) |
20 |
|
eqid |
⊢ dom 𝑅 = dom 𝑅 |
21 |
20
|
psref |
⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → 𝑥 𝑅 𝑥 ) |
22 |
19 21
|
syldan |
⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅 ) → 𝑥 𝑅 𝑥 ) |
23 |
22
|
adantrr |
⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 𝑅 𝑥 ) |
24 |
|
brinxp2 |
⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝑥 ) ) |
25 |
15 15 23 24
|
syl21anbrc |
⊢ ( ( 𝑅 ∈ PosetRel ∧ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) |
26 |
25
|
expr |
⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) |
27 |
14 26
|
syl5bi |
⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ ∪ ∪ 𝑅 ) → ( 𝑥 ∈ ∪ ∪ ( 𝐴 × 𝐴 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) |
28 |
27
|
expimpd |
⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 ∈ ∪ ∪ ( 𝐴 × 𝐴 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) |
29 |
12 28
|
syl5bi |
⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ ( ∪ ∪ 𝑅 ∩ ∪ ∪ ( 𝐴 × 𝐴 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) |
30 |
29
|
ralrimiv |
⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∈ ( ∪ ∪ 𝑅 ∩ ∪ ∪ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) |
31 |
|
ssralv |
⊢ ( ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( ∪ ∪ 𝑅 ∩ ∪ ∪ ( 𝐴 × 𝐴 ) ) → ( ∀ 𝑥 ∈ ( ∪ ∪ 𝑅 ∩ ∪ ∪ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 → ∀ 𝑥 ∈ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) |
32 |
11 30 31
|
mpsyl |
⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∈ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) |
33 |
1
|
ssbri |
⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 → 𝑥 𝑅 𝑦 ) |
34 |
1
|
ssbri |
⊢ ( 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 → 𝑦 𝑅 𝑥 ) |
35 |
|
psasym |
⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) |
36 |
35
|
3expib |
⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) |
37 |
33 34 36
|
syl2ani |
⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ) |
38 |
37
|
alrimivv |
⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ) |
39 |
|
asymref2 |
⊢ ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑥 ∈ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ) ) |
40 |
32 38 39
|
sylanbrc |
⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
41 |
|
inex1g |
⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V ) |
42 |
|
isps |
⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel ↔ ( Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) ) |
43 |
41 42
|
syl |
⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel ↔ ( Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ∪ ∪ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) ) |
44 |
4 7 40 43
|
mpbir3and |
⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel ) |