Step | Hyp | Ref
| Expression |
1 | | ordtrest2.2 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ TosetRel ) |
2 | | tsrps 17831 |
. . . 4
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈
PosetRel) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ PosetRel) |
4 | | ordtrest2.1 |
. . . . 5
⊢ 𝑋 = dom 𝑅 |
5 | 1 | dmexd 7615 |
. . . . 5
⊢ (𝜑 → dom 𝑅 ∈ V) |
6 | 4, 5 | eqeltrid 2917 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ V) |
7 | | ordtrest2.3 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
8 | 6, 7 | ssexd 5228 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
9 | | ordtrest 21810 |
. . 3
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ V) →
(ordTop‘(𝑅 ∩
(𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) |
10 | 3, 8, 9 | syl2anc 586 |
. 2
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) |
11 | | eqid 2821 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) = ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) |
12 | | eqid 2821 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) |
13 | 4, 11, 12 | ordtval 21797 |
. . . . . . 7
⊢ (𝑅 ∈ TosetRel →
(ordTop‘𝑅) =
(topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))))) |
14 | 1, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ordTop‘𝑅) =
(topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))))) |
15 | 14 | oveq1d 7171 |
. . . . 5
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) |
16 | | fibas 21585 |
. . . . . 6
⊢
(fi‘({𝑋} ∪
(ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ∈ TopBases |
17 | | tgrest 21767 |
. . . . . 6
⊢
(((fi‘({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ∈ TopBases ∧ 𝐴 ∈ V) →
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) |
18 | 16, 8, 17 | sylancr 589 |
. . . . 5
⊢ (𝜑 →
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) |
19 | 15, 18 | eqtr4d 2859 |
. . . 4
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴))) |
20 | | firest 16706 |
. . . . 5
⊢
(fi‘(({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴)) = ((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴) |
21 | 20 | fveq2i 6673 |
. . . 4
⊢
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) = (topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) |
22 | 19, 21 | syl6eqr 2874 |
. . 3
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴)))) |
23 | | inex1g 5223 |
. . . . . 6
⊢ (𝑅 ∈ TosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) |
24 | 1, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) |
25 | | ordttop 21808 |
. . . . 5
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ Top) |
26 | 24, 25 | syl 17 |
. . . 4
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ Top) |
27 | 4, 11, 12 | ordtuni 21798 |
. . . . . . . . 9
⊢ (𝑅 ∈ TosetRel → 𝑋 = ∪
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) |
28 | 1, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 = ∪ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) |
29 | 28, 6 | eqeltrrd 2914 |
. . . . . . 7
⊢ (𝜑 → ∪ ({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) |
30 | | uniexb 7486 |
. . . . . . 7
⊢ (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V ↔ ∪ ({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) |
31 | 29, 30 | sylibr 236 |
. . . . . 6
⊢ (𝜑 → ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) |
32 | | restval 16700 |
. . . . . 6
⊢ ((({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V ∧ 𝐴 ∈ V) → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴))) |
33 | 31, 8, 32 | syl2anc 586 |
. . . . 5
⊢ (𝜑 → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴))) |
34 | | sseqin2 4192 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴) |
35 | 7, 34 | sylib 220 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∩ 𝐴) = 𝐴) |
36 | | eqid 2821 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝑅 ∩ (𝐴 × 𝐴)) = dom (𝑅 ∩ (𝐴 × 𝐴)) |
37 | 36 | ordttopon 21801 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴)))) |
38 | 24, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴)))) |
39 | 4 | psssdm 17826 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴) |
40 | 3, 7, 39 | syl2anc 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴) |
41 | 40 | fveq2d 6674 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴))) = (TopOn‘𝐴)) |
42 | 38, 41 | eleqtrd 2915 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴)) |
43 | | toponmax 21534 |
. . . . . . . . . . . 12
⊢
((ordTop‘(𝑅
∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴) → 𝐴 ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
45 | 35, 44 | eqeltrd 2913 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
46 | | elsni 4584 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ {𝑋} → 𝑣 = 𝑋) |
47 | 46 | ineq1d 4188 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ {𝑋} → (𝑣 ∩ 𝐴) = (𝑋 ∩ 𝐴)) |
48 | 47 | eleq1d 2897 |
. . . . . . . . . 10
⊢ (𝑣 ∈ {𝑋} → ((𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑋 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
49 | 45, 48 | syl5ibrcom 249 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ {𝑋} → (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
50 | 49 | ralrimiv 3181 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
51 | | ordtrest2.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴) |
52 | 4, 1, 7, 51 | ordtrest2lem 21811 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
53 | | df-rn 5566 |
. . . . . . . . . . 11
⊢ ran 𝑅 = dom ◡𝑅 |
54 | | cnvtsr 17832 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel ) |
55 | 1, 54 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝑅 ∈ TosetRel ) |
56 | 4 | psrn 17819 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅) |
57 | 3, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 = ran 𝑅) |
58 | 7, 57 | sseqtrd 4007 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ran 𝑅) |
59 | 57 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑋 = ran 𝑅) |
60 | 59 | rabeqdv 3484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)}) |
61 | | vex 3497 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
62 | | vex 3497 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
63 | 61, 62 | brcnv 5753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦◡𝑅𝑧 ↔ 𝑧𝑅𝑦) |
64 | | vex 3497 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
65 | 62, 64 | brcnv 5753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧◡𝑅𝑥 ↔ 𝑥𝑅𝑧) |
66 | 63, 65 | anbi12ci 629 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥) ↔ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)) |
67 | 66 | rabbii 3473 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} = {𝑧 ∈ ran 𝑅 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} |
68 | 60, 67 | syl6eqr 2874 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)}) |
69 | 68, 51 | eqsstrrd 4006 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} ⊆ 𝐴) |
70 | 69 | ancom2s 648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} ⊆ 𝐴) |
71 | 53, 55, 58, 70 | ordtrest2lem 21811 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴)))) |
72 | | vex 3497 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑤 ∈ V |
73 | 72, 62 | brcnv 5753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤◡𝑅𝑧 ↔ 𝑧𝑅𝑤) |
74 | 73 | bicomi 226 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧𝑅𝑤 ↔ 𝑤◡𝑅𝑧) |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧𝑅𝑤 ↔ 𝑤◡𝑅𝑧)) |
76 | 75 | notbid 320 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (¬ 𝑧𝑅𝑤 ↔ ¬ 𝑤◡𝑅𝑧)) |
77 | 57, 76 | rabeqbidv 3485 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤} = {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧}) |
78 | 57, 77 | mpteq12dv 5151 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})) |
79 | 78 | rneqd 5808 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})) |
80 | | cnvin 6003 |
. . . . . . . . . . . . . . 15
⊢ ◡(𝑅 ∩ (𝐴 × 𝐴)) = (◡𝑅 ∩ ◡(𝐴 × 𝐴)) |
81 | | cnvxp 6014 |
. . . . . . . . . . . . . . . 16
⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴) |
82 | 81 | ineq2i 4186 |
. . . . . . . . . . . . . . 15
⊢ (◡𝑅 ∩ ◡(𝐴 × 𝐴)) = (◡𝑅 ∩ (𝐴 × 𝐴)) |
83 | 80, 82 | eqtri 2844 |
. . . . . . . . . . . . . 14
⊢ ◡(𝑅 ∩ (𝐴 × 𝐴)) = (◡𝑅 ∩ (𝐴 × 𝐴)) |
84 | 83 | fveq2i 6673 |
. . . . . . . . . . . . 13
⊢
(ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))) |
85 | | psss 17824 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) |
86 | 3, 85 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) |
87 | | ordtcnv 21809 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel →
(ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
89 | 84, 88 | syl5reqr 2871 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴)))) |
90 | 89 | eleq2d 2898 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))))) |
91 | 79, 90 | raleqbidv 3401 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ ∀𝑣 ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))))) |
92 | 71, 91 | mpbird 259 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
93 | | ralunb 4167 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
(ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
94 | 52, 92, 93 | sylanbrc 585 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
95 | | ralunb 4167 |
. . . . . . . 8
⊢
(∀𝑣 ∈
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
96 | 50, 94, 95 | sylanbrc 585 |
. . . . . . 7
⊢ (𝜑 → ∀𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
97 | | eqid 2821 |
. . . . . . . 8
⊢ (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) = (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) |
98 | 97 | fmpt 6874 |
. . . . . . 7
⊢
(∀𝑣 ∈
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))⟶(ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
99 | 96, 98 | sylib 220 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))⟶(ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
100 | 99 | frnd 6521 |
. . . . 5
⊢ (𝜑 → ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
101 | 33, 100 | eqsstrd 4005 |
. . . 4
⊢ (𝜑 → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
102 | | tgfiss 21599 |
. . . 4
⊢
(((ordTop‘(𝑅
∩ (𝐴 × 𝐴))) ∈ Top ∧ (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) → (topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
103 | 26, 101, 102 | syl2anc 586 |
. . 3
⊢ (𝜑 →
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
104 | 22, 103 | eqsstrd 4005 |
. 2
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
105 | 10, 104 | eqssd 3984 |
1
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = ((ordTop‘𝑅) ↾t 𝐴)) |