Step |
Hyp |
Ref |
Expression |
1 |
|
ordtrest2.1 |
⊢ 𝑋 = dom 𝑅 |
2 |
|
ordtrest2.2 |
⊢ ( 𝜑 → 𝑅 ∈ TosetRel ) |
3 |
|
ordtrest2.3 |
⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 ) |
4 |
|
ordtrest2.4 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 ) |
5 |
|
inrab2 |
⊢ ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) = { 𝑤 ∈ ( 𝑋 ∩ 𝐴 ) ∣ ¬ 𝑤 𝑅 𝑧 } |
6 |
|
sseqin2 |
⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝐴 ) = 𝐴 ) |
7 |
3 6
|
sylib |
⊢ ( 𝜑 → ( 𝑋 ∩ 𝐴 ) = 𝐴 ) |
8 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑋 ∩ 𝐴 ) = 𝐴 ) |
9 |
8
|
rabeqdv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → { 𝑤 ∈ ( 𝑋 ∩ 𝐴 ) ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ) |
10 |
5 9
|
eqtrid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ) |
11 |
|
inex1g |
⊢ ( 𝑅 ∈ TosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V ) |
12 |
2 11
|
syl |
⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V ) |
13 |
|
eqid |
⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) |
14 |
13
|
ordttopon |
⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
15 |
12 14
|
syl |
⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
16 |
|
tsrps |
⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel ) |
17 |
2 16
|
syl |
⊢ ( 𝜑 → 𝑅 ∈ PosetRel ) |
18 |
1
|
psssdm |
⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 ) |
19 |
17 3 18
|
syl2anc |
⊢ ( 𝜑 → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 ) |
20 |
19
|
fveq2d |
⊢ ( 𝜑 → ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( TopOn ‘ 𝐴 ) ) |
21 |
15 20
|
eleqtrd |
⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) ) |
22 |
|
toponmax |
⊢ ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
23 |
21 22
|
syl |
⊢ ( 𝜑 → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
24 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
25 |
|
rabid2 |
⊢ ( 𝐴 = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ↔ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 ) |
26 |
|
eleq1 |
⊢ ( 𝐴 = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } → ( 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
27 |
25 26
|
sylbir |
⊢ ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 → ( 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
28 |
24 27
|
syl5ibcom |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
29 |
|
dfrex2 |
⊢ ( ∃ 𝑤 ∈ 𝐴 𝑤 𝑅 𝑧 ↔ ¬ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 ) |
30 |
|
breq1 |
⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝑅 𝑧 ↔ 𝑥 𝑅 𝑧 ) ) |
31 |
30
|
cbvrexvw |
⊢ ( ∃ 𝑤 ∈ 𝐴 𝑤 𝑅 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑧 ) |
32 |
29 31
|
bitr3i |
⊢ ( ¬ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑧 ) |
33 |
|
ordttop |
⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top ) |
34 |
12 33
|
syl |
⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top ) |
35 |
34
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top ) |
36 |
|
0opn |
⊢ ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top → ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
37 |
35 36
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
38 |
37
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
39 |
|
eleq1 |
⊢ ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = ∅ → ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
40 |
38 39
|
syl5ibrcom |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = ∅ → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
41 |
|
rabn0 |
⊢ ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ≠ ∅ ↔ ∃ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 ) |
42 |
|
breq1 |
⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑧 ↔ 𝑦 𝑅 𝑧 ) ) |
43 |
42
|
notbid |
⊢ ( 𝑤 = 𝑦 → ( ¬ 𝑤 𝑅 𝑧 ↔ ¬ 𝑦 𝑅 𝑧 ) ) |
44 |
43
|
cbvrexvw |
⊢ ( ∃ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) |
45 |
41 44
|
bitri |
⊢ ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) |
46 |
2
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑅 ∈ TosetRel ) |
47 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → 𝐴 ⊆ 𝑋 ) |
48 |
47
|
sselda |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝑋 ) |
49 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝑋 ) |
50 |
1
|
tsrlin |
⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑅 𝑧 ∨ 𝑧 𝑅 𝑦 ) ) |
51 |
46 48 49 50
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑧 ∨ 𝑧 𝑅 𝑦 ) ) |
52 |
51
|
ord |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑦 𝑅 𝑧 → 𝑧 𝑅 𝑦 ) ) |
53 |
|
an4 |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) ) ) |
54 |
|
rabss |
⊢ ( { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) ) |
55 |
4 54
|
sylib |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) ) |
56 |
55
|
r19.21bi |
⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) ) |
57 |
56
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) ) |
58 |
57
|
impr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) ) ) → 𝑧 ∈ 𝐴 ) |
59 |
53 58
|
sylan2b |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → 𝑧 ∈ 𝐴 ) |
60 |
|
brinxp |
⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 𝑅 𝑧 ↔ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) |
61 |
60
|
ancoms |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 𝑅 𝑧 ↔ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) |
62 |
61
|
notbid |
⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ 𝑤 𝑅 𝑧 ↔ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) |
63 |
62
|
rabbidva |
⊢ ( 𝑧 ∈ 𝐴 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ) |
64 |
59 63
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ) |
65 |
19
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 ) |
66 |
65
|
rabeqdv |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ) |
67 |
64 66
|
eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ) |
68 |
12
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V ) |
69 |
59 65
|
eleqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → 𝑧 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) |
70 |
13
|
ordtopn1 |
⊢ ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V ∧ 𝑧 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
71 |
68 69 70
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
72 |
67 71
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
73 |
72
|
anassrs |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
74 |
73
|
expr |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 𝑅 𝑦 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
75 |
52 74
|
syld |
⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑦 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
76 |
75
|
rexlimdva |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
77 |
45 76
|
syl5bi |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ≠ ∅ → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
78 |
40 77
|
pm2.61dne |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
79 |
78
|
rexlimdvaa |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
80 |
32 79
|
syl5bi |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ¬ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
81 |
28 80
|
pm2.61d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
82 |
10 81
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
83 |
82
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |
84 |
2
|
dmexd |
⊢ ( 𝜑 → dom 𝑅 ∈ V ) |
85 |
1 84
|
eqeltrid |
⊢ ( 𝜑 → 𝑋 ∈ V ) |
86 |
|
rabexg |
⊢ ( 𝑋 ∈ V → { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V ) |
87 |
85 86
|
syl |
⊢ ( 𝜑 → { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V ) |
88 |
87
|
ralrimivw |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V ) |
89 |
|
eqid |
⊢ ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) = ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) |
90 |
|
ineq1 |
⊢ ( 𝑣 = { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } → ( 𝑣 ∩ 𝐴 ) = ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ) |
91 |
90
|
eleq1d |
⊢ ( 𝑣 = { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
92 |
89 91
|
ralrnmptw |
⊢ ( ∀ 𝑧 ∈ 𝑋 { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V → ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
93 |
88 92
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) |
94 |
83 93
|
mpbird |
⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) |