Proof of Theorem ordtrest2NEWlem
| Step | Hyp | Ref
| Expression |
| 1 | | inrab2 4317 |
. . . . 5
⊢ ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) = {𝑤 ∈ (𝐵 ∩ 𝐴) ∣ ¬ 𝑤 ≤ 𝑧} |
| 2 | | ordtrest2NEW.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| 3 | | sseqin2 4223 |
. . . . . . . 8
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∩ 𝐴) = 𝐴) |
| 4 | 2, 3 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∩ 𝐴) = 𝐴) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐵 ∩ 𝐴) = 𝐴) |
| 6 | | rabeq 3451 |
. . . . . 6
⊢ ((𝐵 ∩ 𝐴) = 𝐴 → {𝑤 ∈ (𝐵 ∩ 𝐴) ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧}) |
| 7 | 5, 6 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → {𝑤 ∈ (𝐵 ∩ 𝐴) ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧}) |
| 8 | 1, 7 | eqtrid 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧}) |
| 9 | | ordtNEW.l |
. . . . . . . . . . . . 13
⊢ ≤ =
((le‘𝐾) ∩ (𝐵 × 𝐵)) |
| 10 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(le‘𝐾) ∈
V |
| 11 | 10 | inex1 5317 |
. . . . . . . . . . . . 13
⊢
((le‘𝐾) ∩
(𝐵 × 𝐵)) ∈ V |
| 12 | 9, 11 | eqeltri 2837 |
. . . . . . . . . . . 12
⊢ ≤ ∈
V |
| 13 | 12 | inex1 5317 |
. . . . . . . . . . 11
⊢ ( ≤ ∩
(𝐴 × 𝐴)) ∈ V |
| 14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ( ≤ ∩ (𝐴 × 𝐴)) ∈ V) |
| 15 | | eqid 2737 |
. . . . . . . . . . 11
⊢ dom (
≤
∩ (𝐴 × 𝐴)) = dom ( ≤ ∩ (𝐴 × 𝐴)) |
| 16 | 15 | ordttopon 23201 |
. . . . . . . . . 10
⊢ (( ≤ ∩
(𝐴 × 𝐴)) ∈ V →
(ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘dom ( ≤ ∩
(𝐴 × 𝐴)))) |
| 17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) ∈ (TopOn‘dom (
≤
∩ (𝐴 × 𝐴)))) |
| 18 | | ordtrest2NEW.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ Toset) |
| 19 | | tospos 18465 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset) |
| 20 | | posprs 18362 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset
) |
| 21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ Proset ) |
| 22 | | ordtNEW.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐾) |
| 23 | 22, 9 | prsssdm 33916 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) |
| 24 | 21, 2, 23 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) |
| 25 | 24 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 → (TopOn‘dom ( ≤ ∩
(𝐴 × 𝐴))) = (TopOn‘𝐴)) |
| 26 | 17, 25 | eleqtrd 2843 |
. . . . . . . 8
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) ∈ (TopOn‘𝐴)) |
| 27 | | toponmax 22932 |
. . . . . . . 8
⊢
((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ (TopOn‘𝐴) → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 30 | | rabid2 3470 |
. . . . . . 7
⊢ (𝐴 = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ↔ ∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧) |
| 31 | | eleq1 2829 |
. . . . . . 7
⊢ (𝐴 = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} → (𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 32 | 30, 31 | sylbir 235 |
. . . . . 6
⊢
(∀𝑤 ∈
𝐴 ¬ 𝑤 ≤ 𝑧 → (𝐴 ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 33 | 29, 32 | syl5ibcom 245 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 34 | | dfrex2 3073 |
. . . . . . 7
⊢
(∃𝑤 ∈
𝐴 𝑤 ≤ 𝑧 ↔ ¬ ∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧) |
| 35 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤 ≤ 𝑧 ↔ 𝑥 ≤ 𝑧)) |
| 36 | 35 | cbvrexvw 3238 |
. . . . . . 7
⊢
(∃𝑤 ∈
𝐴 𝑤 ≤ 𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑧) |
| 37 | 34, 36 | bitr3i 277 |
. . . . . 6
⊢ (¬
∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 ↔ ∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑧) |
| 38 | | ordttop 23208 |
. . . . . . . . . . . . 13
⊢ (( ≤ ∩
(𝐴 × 𝐴)) ∈ V →
(ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top) |
| 39 | 14, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ordTop‘( ≤ ∩
(𝐴 × 𝐴))) ∈ Top) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top) |
| 41 | | 0opn 22910 |
. . . . . . . . . . 11
⊢
((ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ∈ Top → ∅ ∈
(ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 42 | 40, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ∅ ∈ (ordTop‘(
≤
∩ (𝐴 × 𝐴)))) |
| 43 | 42 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → ∅ ∈ (ordTop‘(
≤
∩ (𝐴 × 𝐴)))) |
| 44 | | eleq1 2829 |
. . . . . . . . 9
⊢ ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = ∅ → ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∅ ∈ (ordTop‘(
≤
∩ (𝐴 × 𝐴))))) |
| 45 | 43, 44 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = ∅ → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 46 | | rabn0 4389 |
. . . . . . . . . 10
⊢ ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧) |
| 47 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → (𝑤 ≤ 𝑧 ↔ 𝑦 ≤ 𝑧)) |
| 48 | 47 | notbid 318 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑦 → (¬ 𝑤 ≤ 𝑧 ↔ ¬ 𝑦 ≤ 𝑧)) |
| 49 | 48 | cbvrexvw 3238 |
. . . . . . . . . 10
⊢
(∃𝑤 ∈
𝐴 ¬ 𝑤 ≤ 𝑧 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑧) |
| 50 | 46, 49 | bitri 275 |
. . . . . . . . 9
⊢ ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ≠ ∅ ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑧) |
| 51 | 18 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Toset) |
| 52 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → 𝐴 ⊆ 𝐵) |
| 53 | 52 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵) |
| 54 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐵) |
| 55 | 22, 9 | trleile 32961 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Toset ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦 ≤ 𝑧 ∨ 𝑧 ≤ 𝑦)) |
| 56 | 51, 53, 54, 55 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ 𝑧 ∨ 𝑧 ≤ 𝑦)) |
| 57 | 56 | ord 865 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (¬ 𝑦 ≤ 𝑧 → 𝑧 ≤ 𝑦)) |
| 58 | | an4 656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) |
| 59 | | ordtrest2NEW.4 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) |
| 60 | | rabss 4072 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴 ↔ ∀𝑧 ∈ 𝐵 ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴)) |
| 61 | 59, 60 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ∀𝑧 ∈ 𝐵 ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴)) |
| 62 | 61 | r19.21bi 3251 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴)) |
| 63 | 62 | an32s 652 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦) → 𝑧 ∈ 𝐴)) |
| 64 | 63 | impr 454 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦))) → 𝑧 ∈ 𝐴) |
| 65 | 58, 64 | sylan2b 594 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → 𝑧 ∈ 𝐴) |
| 66 | | brinxp 5764 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑤 ≤ 𝑧 ↔ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧)) |
| 67 | 66 | ancoms 458 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑤 ≤ 𝑧 ↔ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧)) |
| 68 | 67 | notbid 318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 ≤ 𝑧 ↔ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧)) |
| 69 | 68 | rabbidva 3443 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝐴 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧}) |
| 70 | 65, 69 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧}) |
| 71 | 24 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) |
| 72 | | rabeq 3451 |
. . . . . . . . . . . . . . . 16
⊢ (dom (
≤
∩ (𝐴 × 𝐴)) = 𝐴 → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧}) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} = {𝑤 ∈ 𝐴 ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧}) |
| 74 | 70, 73 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} = {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧}) |
| 75 | 13 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → ( ≤ ∩ (𝐴 × 𝐴)) ∈ V) |
| 76 | 65, 71 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → 𝑧 ∈ dom ( ≤ ∩ (𝐴 × 𝐴))) |
| 77 | 15 | ordtopn1 23202 |
. . . . . . . . . . . . . . 15
⊢ ((( ≤ ∩
(𝐴 × 𝐴)) ∈ V ∧ 𝑧 ∈ dom ( ≤ ∩ (𝐴 × 𝐴))) → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 78 | 75, 76, 77 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ dom ( ≤ ∩ (𝐴 × 𝐴)) ∣ ¬ 𝑤( ≤ ∩ (𝐴 × 𝐴))𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 79 | 74, 78 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦))) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 80 | 79 | anassrs 467 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ≤ 𝑦)) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 81 | 80 | expr 456 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (𝑧 ≤ 𝑦 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 82 | 57, 81 | syld 47 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) ∧ 𝑦 ∈ 𝐴) → (¬ 𝑦 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 83 | 82 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → (∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 84 | 50, 83 | biimtrid 242 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → ({𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ≠ ∅ → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 85 | 45, 84 | pm2.61dne 3028 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑧)) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 86 | 85 | rexlimdvaa 3156 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 87 | 37, 86 | biimtrid 242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (¬ ∀𝑤 ∈ 𝐴 ¬ 𝑤 ≤ 𝑧 → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 88 | 33, 87 | pm2.61d 179 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → {𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ≤ 𝑧} ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 89 | 8, 88 | eqeltrd 2841 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 90 | 89 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |
| 91 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝐾)
∈ V |
| 92 | 22, 91 | eqeltri 2837 |
. . . . . 6
⊢ 𝐵 ∈ V |
| 93 | 92 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
| 94 | | rabexg 5337 |
. . . . 5
⊢ (𝐵 ∈ V → {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V) |
| 95 | 93, 94 | syl 17 |
. . . 4
⊢ (𝜑 → {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V) |
| 96 | 95 | ralrimivw 3150 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V) |
| 97 | | eqid 2737 |
. . . 4
⊢ (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) = (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧}) |
| 98 | | ineq1 4213 |
. . . . 5
⊢ (𝑣 = {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} → (𝑣 ∩ 𝐴) = ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴)) |
| 99 | 98 | eleq1d 2826 |
. . . 4
⊢ (𝑣 = {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} → ((𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 100 | 97, 99 | ralrnmptw 7114 |
. . 3
⊢
(∀𝑧 ∈
𝐵 {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∈ V → (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∀𝑧 ∈ 𝐵 ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 101 | 96, 100 | syl 17 |
. 2
⊢ (𝜑 → (∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ↔ ∀𝑧 ∈ 𝐵 ({𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧} ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))) |
| 102 | 90, 101 | mpbird 257 |
1
⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) |