Step | Hyp | Ref
| Expression |
1 | | ordtrest2NEW.2 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Toset) |
2 | | tospos 28989 |
. . . 4
⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset) |
3 | | posprs 16772 |
. . . 4
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Preset
) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Preset ) |
5 | | ordtrest2NEW.3 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
6 | | ordtNEW.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
7 | | ordtNEW.l |
. . . 4
⊢ ≤ =
((le‘𝐾) ∩ (𝐵 × 𝐵)) |
8 | 6, 7 | ordtrestNEW 29295 |
. . 3
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ )
↾t 𝐴)) |
9 | 4, 5, 8 | syl2anc 691 |
. 2
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) ⊆ ((ordTop‘
≤ )
↾t 𝐴)) |
10 | | eqid 2610 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) = ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) |
11 | | eqid 2610 |
. . . . . . . 8
⊢ ran
(𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}) = ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}) |
12 | 6, 7, 10, 11 | ordtprsval 29292 |
. . . . . . 7
⊢ (𝐾 ∈ Preset →
(ordTop‘ ≤ ) =
(topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))))) |
13 | 4, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → (ordTop‘ ≤ ) =
(topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))))) |
14 | 13 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t 𝐴) =
((topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))) ↾t 𝐴)) |
15 | | fibas 20592 |
. . . . . 6
⊢
(fi‘({𝐵} ∪
(ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ∈ TopBases |
16 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝐾)
∈ V |
17 | 6, 16 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
19 | 18, 5 | ssexd 4733 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
20 | | tgrest 20773 |
. . . . . 6
⊢
(((fi‘({𝐵}
∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ∈ TopBases ∧ 𝐴 ∈ V) →
(topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))) ↾t 𝐴)) |
21 | 15, 19, 20 | sylancr 694 |
. . . . 5
⊢ (𝜑 →
(topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴)) = ((topGen‘(fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))))) ↾t 𝐴)) |
22 | 14, 21 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t 𝐴) =
(topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴))) |
23 | | firest 15916 |
. . . . 5
⊢
(fi‘(({𝐵}
∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴)) = ((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴) |
24 | 23 | fveq2i 6106 |
. . . 4
⊢
(topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴))) = (topGen‘((fi‘({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) ↾t 𝐴)) |
25 | 22, 24 | syl6eqr 2662 |
. . 3
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t 𝐴) =
(topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴)))) |
26 | | fvex 6113 |
. . . . . . . 8
⊢
(le‘𝐾) ∈
V |
27 | 26 | inex1 4727 |
. . . . . . 7
⊢
((le‘𝐾) ∩
(𝐵 × 𝐵)) ∈ V |
28 | 7, 27 | eqeltri 2684 |
. . . . . 6
⊢ ≤ ∈
V |
29 | 28 | inex1 4727 |
. . . . 5
⊢ ( ≤ ∩
(𝐴 × 𝐴)) ∈ V |
30 | | ordttop 20814 |
. . . . 5
⊢ (( ≤ ∩
(𝐴 × 𝐴)) ∈ V →
(ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top) |
31 | 29, 30 | mp1i 13 |
. . . 4
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) ∈ Top) |
32 | 6, 7, 10, 11 | ordtprsuni 29293 |
. . . . . . . . 9
⊢ (𝐾 ∈ Preset → 𝐵 = ∪
({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) |
33 | 4, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = ∪ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))) |
34 | 33, 18 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → ∪ ({𝐵}
∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V) |
35 | | uniexb 6866 |
. . . . . . 7
⊢ (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V ↔ ∪ ({𝐵}
∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V) |
36 | 34, 35 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V) |
37 | | restval 15910 |
. . . . . 6
⊢ ((({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ∈ V ∧ 𝐴 ∈ V) → (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴))) |
38 | 36, 19, 37 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) = ran (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴))) |
39 | | sseqin2 3779 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) |
40 | 5, 39 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∩ 𝐴) = 𝐴) |
41 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ dom (
≤
∩ (𝐴 × 𝐴)) = dom ( ≤ ∩ (𝐴 × 𝐴)) |
42 | 41 | ordttopon 20807 |
. . . . . . . . . . . . . 14
⊢ (( ≤ ∩
(𝐴 × 𝐴)) ∈ V →
(ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom ( ≤ ∩
(𝐴 × 𝐴)))) |
43 | 29, 42 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) ∈ (TopOn‘dom (
≤
∩ (𝐴 × 𝐴)))) |
44 | 6, 7 | prsssdm 29291 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) |
45 | 4, 5, 44 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) |
46 | 45 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (TopOn‘dom ( ≤ ∩
(𝐴 × 𝐴))) = (TopOn‘𝐴)) |
47 | 43, 46 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) ∈ (TopOn‘𝐴)) |
48 | | toponmax 20543 |
. . . . . . . . . . . 12
⊢
((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴) → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
50 | 40, 49 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
51 | | elsni 4142 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ {𝐵} → 𝑣 = 𝐵) |
52 | 51 | ineq1d 3775 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ {𝐵} → (𝑣 ∩ 𝐴) = (𝐵 ∩ 𝐴)) |
53 | 52 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑣 ∈ {𝐵} → ((𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (𝐵 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
54 | 50, 53 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ {𝐵} → (𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
55 | 54 | ralrimiv 2948 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ {𝐵} (𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
56 | | ordtrest2NEW.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) |
57 | 6, 7, 1, 5, 56 | ordtrest2NEWlem 29296 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
58 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(ODual‘𝐾) =
(ODual‘𝐾) |
59 | 58, 6 | odubas 16956 |
. . . . . . . . . . 11
⊢ 𝐵 =
(Base‘(ODual‘𝐾)) |
60 | 7 | cnveqi 5219 |
. . . . . . . . . . . 12
⊢ ◡ ≤ = ◡((le‘𝐾) ∩ (𝐵 × 𝐵)) |
61 | | cnvin 5459 |
. . . . . . . . . . . . 13
⊢ ◡((le‘𝐾) ∩ (𝐵 × 𝐵)) = (◡(le‘𝐾) ∩ ◡(𝐵 × 𝐵)) |
62 | | cnvxp 5470 |
. . . . . . . . . . . . . 14
⊢ ◡(𝐵 × 𝐵) = (𝐵 × 𝐵) |
63 | 62 | ineq2i 3773 |
. . . . . . . . . . . . 13
⊢ (◡(le‘𝐾) ∩ ◡(𝐵 × 𝐵)) = (◡(le‘𝐾) ∩ (𝐵 × 𝐵)) |
64 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(le‘𝐾) =
(le‘𝐾) |
65 | 58, 64 | oduleval 16954 |
. . . . . . . . . . . . . 14
⊢ ◡(le‘𝐾) = (le‘(ODual‘𝐾)) |
66 | 65 | ineq1i 3772 |
. . . . . . . . . . . . 13
⊢ (◡(le‘𝐾) ∩ (𝐵 × 𝐵)) = ((le‘(ODual‘𝐾)) ∩ (𝐵 × 𝐵)) |
67 | 61, 63, 66 | 3eqtri 2636 |
. . . . . . . . . . . 12
⊢ ◡((le‘𝐾) ∩ (𝐵 × 𝐵)) = ((le‘(ODual‘𝐾)) ∩ (𝐵 × 𝐵)) |
68 | 60, 67 | eqtri 2632 |
. . . . . . . . . . 11
⊢ ◡ ≤ =
((le‘(ODual‘𝐾))
∩ (𝐵 × 𝐵)) |
69 | 58 | odutos 28994 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ Toset →
(ODual‘𝐾) ∈
Toset) |
70 | 1, 69 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ODual‘𝐾) ∈ Toset) |
71 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
72 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
73 | 71, 72 | brcnv 5227 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑦) |
74 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
75 | 72, 74 | brcnv 5227 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧◡ ≤ 𝑥 ↔ 𝑥 ≤ 𝑧) |
76 | 73, 75 | anbi12ci 730 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦◡ ≤ 𝑧 ∧ 𝑧◡
≤
𝑥) ↔ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐵 → ((𝑦◡
≤
𝑧 ∧ 𝑧◡
≤
𝑥) ↔ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) |
78 | 77 | rabbiia 3161 |
. . . . . . . . . . . . 13
⊢ {𝑧 ∈ 𝐵 ∣ (𝑦◡
≤
𝑧 ∧ 𝑧◡
≤
𝑥)} = {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} |
79 | 78, 56 | syl5eqss 3612 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑦◡
≤
𝑧 ∧ 𝑧◡
≤
𝑥)} ⊆ 𝐴) |
80 | 79 | ancom2s 840 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑦◡
≤
𝑧 ∧ 𝑧◡
≤
𝑥)} ⊆ 𝐴) |
81 | 59, 68, 70, 5, 80 | ordtrest2NEWlem 29296 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡
≤
𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴)))) |
82 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑤 ∈ V |
83 | 82, 72 | brcnv 5227 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑤) |
84 | 83 | bicomi 213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ≤ 𝑤 ↔ 𝑤◡
≤
𝑧) |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧 ≤ 𝑤 ↔ 𝑤◡
≤
𝑧)) |
86 | 85 | notbid 307 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (¬ 𝑧 ≤ 𝑤 ↔ ¬ 𝑤◡
≤
𝑧)) |
87 | 86 | rabbidv 3164 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤} = {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡
≤
𝑧}) |
88 | 87 | mpteq2dv 4673 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}) = (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡
≤
𝑧})) |
89 | 88 | rneqd 5274 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}) = ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡
≤
𝑧})) |
90 | | cnvin 5459 |
. . . . . . . . . . . . . . 15
⊢ ◡( ≤ ∩ (𝐴 × 𝐴)) = (◡ ≤ ∩ ◡(𝐴 × 𝐴)) |
91 | | cnvxp 5470 |
. . . . . . . . . . . . . . . 16
⊢ ◡(𝐴 × 𝐴) = (𝐴 × 𝐴) |
92 | 91 | ineq2i 3773 |
. . . . . . . . . . . . . . 15
⊢ (◡ ≤ ∩ ◡(𝐴 × 𝐴)) = (◡ ≤ ∩ (𝐴 × 𝐴)) |
93 | 90, 92 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ ◡( ≤ ∩ (𝐴 × 𝐴)) = (◡ ≤ ∩ (𝐴 × 𝐴)) |
94 | 93 | fveq2i 6106 |
. . . . . . . . . . . . 13
⊢
(ordTop‘◡( ≤ ∩
(𝐴 × 𝐴))) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))) |
95 | 6 | ressprs 28986 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Preset ) |
96 | 4, 5, 95 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾 ↾s 𝐴) ∈ Preset ) |
97 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘(𝐾
↾s 𝐴)) =
(Base‘(𝐾
↾s 𝐴)) |
98 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
((le‘(𝐾
↾s 𝐴))
∩ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) =
((le‘(𝐾
↾s 𝐴))
∩ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))) |
99 | 97, 98 | ordtcnvNEW 29294 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ↾s 𝐴) ∈ Preset →
(ordTop‘◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) =
(ordTop‘((le‘(𝐾
↾s 𝐴))
∩ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))))) |
100 | 96, 99 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ordTop‘◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) = (ordTop‘((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))))) |
101 | 6, 7 | prsss 29290 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) |
102 | 4, 5, 101 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) |
103 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ↾s 𝐴) = (𝐾 ↾s 𝐴) |
104 | 103, 64 | ressle 15882 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ V → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
105 | 19, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
106 | 103, 6 | ressbas2 15758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) |
107 | 5, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) |
108 | 107 | sqxpeqd 5065 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 × 𝐴) = ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))) |
109 | 105, 108 | ineq12d 3777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((le‘𝐾) ∩ (𝐴 × 𝐴)) = ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) |
110 | 102, 109 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) |
111 | 110 | cnveqd 5220 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡( ≤ ∩ (𝐴 × 𝐴)) = ◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴))))) |
112 | 111 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ordTop‘◡( ≤ ∩ (𝐴 × 𝐴))) = (ordTop‘◡((le‘(𝐾 ↾s 𝐴)) ∩ ((Base‘(𝐾 ↾s 𝐴)) × (Base‘(𝐾 ↾s 𝐴)))))) |
113 | 110 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) =
(ordTop‘((le‘(𝐾
↾s 𝐴))
∩ ((Base‘(𝐾
↾s 𝐴))
× (Base‘(𝐾
↾s 𝐴)))))) |
114 | 100, 112,
113 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ordTop‘◡( ≤ ∩ (𝐴 × 𝐴))) = (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
115 | 94, 114 | syl5reqr 2659 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴)))) |
116 | 115 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∩ 𝐴) ∈ (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))))) |
117 | 89, 116 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤◡
≤
𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))))) |
118 | 81, 117 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
119 | | ralunb 3756 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
(ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
120 | 57, 118, 119 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑣 ∈ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
121 | | ralunb 3756 |
. . . . . . . 8
⊢
(∀𝑣 ∈
({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (∀𝑣 ∈ {𝐵} (𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∧ ∀𝑣 ∈ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
122 | 55, 120, 121 | sylanbrc 695 |
. . . . . . 7
⊢ (𝜑 → ∀𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
123 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)) = (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)) |
124 | 123 | fmpt 6289 |
. . . . . . 7
⊢
(∀𝑣 ∈
({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))⟶(ordTop‘( ≤ ∩
(𝐴 × 𝐴)))) |
125 | 122, 124 | sylib 207 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))⟶(ordTop‘( ≤ ∩
(𝐴 × 𝐴)))) |
126 | | frn 5966 |
. . . . . 6
⊢ ((𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)):({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤})))⟶(ordTop‘( ≤ ∩
(𝐴 × 𝐴))) → ran (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)) ⊆ (ordTop‘( ≤ ∩
(𝐴 × 𝐴)))) |
127 | 125, 126 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑣 ∈ ({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↦ (𝑣 ∩ 𝐴)) ⊆ (ordTop‘( ≤ ∩
(𝐴 × 𝐴)))) |
128 | 38, 127 | eqsstrd 3602 |
. . . 4
⊢ (𝜑 → (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
129 | | tgfiss 20606 |
. . . 4
⊢
(((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top ∧ (({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴) ⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) → (topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘( ≤ ∩
(𝐴 × 𝐴)))) |
130 | 31, 128, 129 | syl2anc 691 |
. . 3
⊢ (𝜑 →
(topGen‘(fi‘(({𝐵} ∪ (ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) ∪ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤}))) ↾t 𝐴))) ⊆ (ordTop‘( ≤ ∩
(𝐴 × 𝐴)))) |
131 | 25, 130 | eqsstrd 3602 |
. 2
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t 𝐴)
⊆ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
132 | 9, 131 | eqssd 3585 |
1
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) = ((ordTop‘ ≤ )
↾t 𝐴)) |