Step | Hyp | Ref
| Expression |
1 | | ordtrest2.2 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ TosetRel ) |
2 | | tsrps 17221 |
. . . 4
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈
PosetRel) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ PosetRel) |
4 | | ordtrest2.1 |
. . . . 5
⊢ 𝑋 = dom 𝑅 |
5 | | dmexg 7097 |
. . . . . 6
⊢ (𝑅 ∈ TosetRel → dom
𝑅 ∈
V) |
6 | 1, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → dom 𝑅 ∈ V) |
7 | 4, 6 | syl5eqel 2705 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ V) |
8 | | ordtrest2.3 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
9 | 7, 8 | ssexd 4805 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
10 | | ordtrest 21006 |
. . 3
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ V) →
(ordTop‘(𝑅 ∩
(𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) |
11 | 3, 9, 10 | syl2anc 693 |
. 2
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴)) |
12 | | eqid 2622 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) = ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) |
13 | | eqid 2622 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) |
14 | 4, 12, 13 | ordtval 20993 |
. . . . . . 7
⊢ (𝑅 ∈ TosetRel →
(ordTop‘𝑅) =
(topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))))) |
15 | 1, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ordTop‘𝑅) =
(topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))))) |
16 | 15 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) |
17 | | fibas 20781 |
. . . . . 6
⊢
(fi‘({𝑋} ∪
(ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ∈ TopBases |
18 | | tgrest 20963 |
. . . . . 6
⊢
(((fi‘({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ∈ TopBases ∧ 𝐴 ∈ V) →
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) |
19 | 17, 9, 18 | sylancr 695 |
. . . . 5
⊢ (𝜑 →
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))))) ↾t 𝐴)) |
20 | 16, 19 | eqtr4d 2659 |
. . . 4
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
(topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴))) |
21 | | firest 16093 |
. . . . 5
⊢
(fi‘(({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴)) = ((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴) |
22 | 21 | fveq2i 6194 |
. . . 4
⊢
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) = (topGen‘((fi‘({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) ↾t 𝐴)) |
23 | 20, 22 | syl6eqr 2674 |
. . 3
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) =
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴)))) |
24 | | inex1g 4801 |
. . . . . 6
⊢ (𝑅 ∈ TosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) |
25 | 1, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V) |
26 | | ordttop 21004 |
. . . . 5
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ Top) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ Top) |
28 | 4, 12, 13 | ordtuni 20994 |
. . . . . . . . 9
⊢ (𝑅 ∈ TosetRel → 𝑋 = ∪
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) |
29 | 1, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 = ∪ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))) |
30 | 29, 7 | eqeltrrd 2702 |
. . . . . . 7
⊢ (𝜑 → ∪ ({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) |
31 | | uniexb 6973 |
. . . . . . 7
⊢ (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V ↔ ∪ ({𝑋}
∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) |
32 | 30, 31 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V) |
33 | | restval 16087 |
. . . . . 6
⊢ ((({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ∈ V ∧ 𝐴 ∈ V) → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴))) |
34 | 32, 9, 33 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴))) |
35 | | sseqin2 3817 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴) |
36 | 8, 35 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∩ 𝐴) = 𝐴) |
37 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝑅 ∩ (𝐴 × 𝐴)) = dom (𝑅 ∩ (𝐴 × 𝐴)) |
38 | 37 | ordttopon 20997 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴)))) |
39 | 25, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴)))) |
40 | 4 | psssdm 17216 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴) |
41 | 3, 8, 40 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴) |
42 | 41 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (TopOn‘dom (𝑅 ∩ (𝐴 × 𝐴))) = (TopOn‘𝐴)) |
43 | 39, 42 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴)) |
44 | | toponmax 20730 |
. . . . . . . . . . . 12
⊢
((ordTop‘(𝑅
∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴) → 𝐴 ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
46 | 36, 45 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
47 | | elsni 4194 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ {𝑋} → 𝑣 = 𝑋) |
48 | 47 | ineq1d 3813 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ {𝑋} → (𝑣 ∩ 𝐴) = (𝑋 ∩ 𝐴)) |
49 | 48 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑣 ∈ {𝑋} → ((𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑋 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
50 | 46, 49 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ {𝑋} → (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
51 | 50 | ralrimiv 2965 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
52 | | ordtrest2.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴) |
53 | 4, 1, 8, 52 | ordtrest2lem 21007 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
54 | | df-rn 5125 |
. . . . . . . . . . 11
⊢ ran 𝑅 = dom ◡𝑅 |
55 | | cnvtsr 17222 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel ) |
56 | 1, 55 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ◡𝑅 ∈ TosetRel ) |
57 | 4 | psrn 17209 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅) |
58 | 3, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 = ran 𝑅) |
59 | 8, 58 | sseqtrd 3641 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ran 𝑅) |
60 | 58 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑋 = ran 𝑅) |
61 | | rabeq 3192 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = ran 𝑅 → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)}) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)}) |
63 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
64 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
65 | 63, 64 | brcnv 5305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦◡𝑅𝑧 ↔ 𝑧𝑅𝑦) |
66 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
67 | 64, 66 | brcnv 5305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧◡𝑅𝑥 ↔ 𝑥𝑅𝑧) |
68 | 65, 67 | anbi12ci 734 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥) ↔ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)) |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ran 𝑅 → ((𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥) ↔ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦))) |
70 | 69 | rabbiia 3185 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} = {𝑧 ∈ ran 𝑅 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} |
71 | 62, 70 | syl6eqr 2674 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} = {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)}) |
72 | 71, 52 | eqsstr3d 3640 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} ⊆ 𝐴) |
73 | 72 | ancom2s 844 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → {𝑧 ∈ ran 𝑅 ∣ (𝑦◡𝑅𝑧 ∧ 𝑧◡𝑅𝑥)} ⊆ 𝐴) |
74 | 54, 56, 59, 73 | ordtrest2lem 21007 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴)))) |
75 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑤 ∈ V |
76 | 75, 64 | brcnv 5305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤◡𝑅𝑧 ↔ 𝑧𝑅𝑤) |
77 | 76 | bicomi 214 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧𝑅𝑤 ↔ 𝑤◡𝑅𝑧) |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧𝑅𝑤 ↔ 𝑤◡𝑅𝑧)) |
79 | 78 | notbid 308 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (¬ 𝑧𝑅𝑤 ↔ ¬ 𝑤◡𝑅𝑧)) |
80 | 58, 79 | rabeqbidv 3195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤} = {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧}) |
81 | 58, 80 | mpteq12dv 4733 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})) |
82 | 81 | rneqd 5353 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}) = ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})) |
83 | | cnvin 5540 |
. . . . . . . . . . . . . . 15
⊢ ◡(𝑅 ∩ (𝐴 × 𝐴)) = (◡𝑅 ∩ ◡(𝐴 × 𝐴)) |
84 | | cnvxp 5551 |
. . . . . . . . . . . . . . . 16
⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴) |
85 | 84 | ineq2i 3811 |
. . . . . . . . . . . . . . 15
⊢ (◡𝑅 ∩ ◡(𝐴 × 𝐴)) = (◡𝑅 ∩ (𝐴 × 𝐴)) |
86 | 83, 85 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ ◡(𝑅 ∩ (𝐴 × 𝐴)) = (◡𝑅 ∩ (𝐴 × 𝐴)) |
87 | 86 | fveq2i 6194 |
. . . . . . . . . . . . 13
⊢
(ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))) |
88 | | psss 17214 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) |
89 | 3, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) |
90 | | ordtcnv 21005 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel →
(ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘◡(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
92 | 87, 91 | syl5reqr 2671 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴)))) |
93 | 92 | eleq2d 2687 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))))) |
94 | 82, 93 | raleqbidv 3152 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ ∀𝑣 ∈ ran (𝑧 ∈ ran 𝑅 ↦ {𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤◡𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡𝑅 ∩ (𝐴 × 𝐴))))) |
95 | 74, 94 | mpbird 247 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
96 | | ralunb 3794 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
(ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
97 | 53, 95, 96 | sylanbrc 698 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
98 | | ralunb 3794 |
. . . . . . . 8
⊢
(∀𝑣 ∈
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ {𝑋} (𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))) |
99 | 51, 97, 98 | sylanbrc 698 |
. . . . . . 7
⊢ (𝜑 → ∀𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
100 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) = (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) |
101 | 100 | fmpt 6381 |
. . . . . . 7
⊢
(∀𝑣 ∈
({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))⟶(ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
102 | 99, 101 | sylib 208 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))⟶(ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
103 | | frn 6053 |
. . . . . 6
⊢ ((𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤})))⟶(ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) → ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
104 | 102, 103 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑣 ∈ ({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↦ (𝑣 ∩ 𝐴)) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
105 | 34, 104 | eqsstrd 3639 |
. . . 4
⊢ (𝜑 → (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
106 | | tgfiss 20795 |
. . . 4
⊢
(((ordTop‘(𝑅
∩ (𝐴 × 𝐴))) ∈ Top ∧ (({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) → (topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
107 | 27, 105, 106 | syl2anc 693 |
. . 3
⊢ (𝜑 →
(topGen‘(fi‘(({𝑋} ∪ (ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧}) ∪ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑧𝑅𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
108 | 23, 107 | eqsstrd 3639 |
. 2
⊢ (𝜑 → ((ordTop‘𝑅) ↾t 𝐴) ⊆ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴)))) |
109 | 11, 108 | eqssd 3620 |
1
⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = ((ordTop‘𝑅) ↾t 𝐴)) |