| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lubsscl.t | . . . 4
⊢ (𝜑 → 𝑇 ⊆ 𝑆) | 
| 2 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 3 |  | eqid 2737 | . . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 4 |  | lubsscl.u | . . . . 5
⊢ 𝑈 = (lub‘𝐾) | 
| 5 |  | lubsscl.k | . . . . 5
⊢ (𝜑 → 𝐾 ∈ Poset) | 
| 6 |  | lubsscl.s | . . . . 5
⊢ (𝜑 → 𝑆 ∈ dom 𝑈) | 
| 7 | 2, 3, 4, 5, 6 | lubelss 18399 | . . . 4
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝐾)) | 
| 8 | 1, 7 | sstrd 3994 | . . 3
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝐾)) | 
| 9 |  | lubsscl.x | . . . . 5
⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝑇) | 
| 10 | 8, 9 | sseldd 3984 | . . . 4
⊢ (𝜑 → (𝑈‘𝑆) ∈ (Base‘𝐾)) | 
| 11 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → 𝐾 ∈ Poset) | 
| 12 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → 𝑆 ∈ dom 𝑈) | 
| 13 | 1 | sselda 3983 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → 𝑦 ∈ 𝑆) | 
| 14 | 2, 3, 4, 11, 12, 13 | luble 18404 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑇) → 𝑦(le‘𝐾)(𝑈‘𝑆)) | 
| 15 | 14 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)(𝑈‘𝑆)) | 
| 16 |  | breq1 5146 | . . . . . . 7
⊢ (𝑦 = (𝑈‘𝑆) → (𝑦(le‘𝐾)𝑧 ↔ (𝑈‘𝑆)(le‘𝐾)𝑧)) | 
| 17 |  | simp3 1139 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧) → ∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧) | 
| 18 | 9 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧) → (𝑈‘𝑆) ∈ 𝑇) | 
| 19 | 16, 17, 18 | rspcdva 3623 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝐾) ∧ ∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧) → (𝑈‘𝑆)(le‘𝐾)𝑧) | 
| 20 | 19 | 3expia 1122 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (Base‘𝐾)) → (∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → (𝑈‘𝑆)(le‘𝐾)𝑧)) | 
| 21 | 20 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → (𝑈‘𝑆)(le‘𝐾)𝑧)) | 
| 22 |  | breq2 5147 | . . . . . . 7
⊢ (𝑥 = (𝑈‘𝑆) → (𝑦(le‘𝐾)𝑥 ↔ 𝑦(le‘𝐾)(𝑈‘𝑆))) | 
| 23 | 22 | ralbidv 3178 | . . . . . 6
⊢ (𝑥 = (𝑈‘𝑆) → (∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑥 ↔ ∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)(𝑈‘𝑆))) | 
| 24 |  | breq1 5146 | . . . . . . . 8
⊢ (𝑥 = (𝑈‘𝑆) → (𝑥(le‘𝐾)𝑧 ↔ (𝑈‘𝑆)(le‘𝐾)𝑧)) | 
| 25 | 24 | imbi2d 340 | . . . . . . 7
⊢ (𝑥 = (𝑈‘𝑆) → ((∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧) ↔ (∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → (𝑈‘𝑆)(le‘𝐾)𝑧))) | 
| 26 | 25 | ralbidv 3178 | . . . . . 6
⊢ (𝑥 = (𝑈‘𝑆) → (∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → (𝑈‘𝑆)(le‘𝐾)𝑧))) | 
| 27 | 23, 26 | anbi12d 632 | . . . . 5
⊢ (𝑥 = (𝑈‘𝑆) → ((∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)(𝑈‘𝑆) ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → (𝑈‘𝑆)(le‘𝐾)𝑧)))) | 
| 28 | 27 | rspcev 3622 | . . . 4
⊢ (((𝑈‘𝑆) ∈ (Base‘𝐾) ∧ (∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)(𝑈‘𝑆) ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → (𝑈‘𝑆)(le‘𝐾)𝑧))) → ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) | 
| 29 | 10, 15, 21, 28 | syl12anc 837 | . . 3
⊢ (𝜑 → ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) | 
| 30 |  | biid 261 | . . . 4
⊢
((∀𝑦 ∈
𝑇 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) | 
| 31 | 2, 3, 4, 30, 5 | lubeldm2 48853 | . . 3
⊢ (𝜑 → (𝑇 ∈ dom 𝑈 ↔ (𝑇 ⊆ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑇 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))))) | 
| 32 | 8, 29, 31 | mpbir2and 713 | . 2
⊢ (𝜑 → 𝑇 ∈ dom 𝑈) | 
| 33 | 3, 2, 4, 5, 8, 10,
14, 19 | poslubd 18458 | . 2
⊢ (𝜑 → (𝑈‘𝑇) = (𝑈‘𝑆)) | 
| 34 | 32, 33 | jca 511 | 1
⊢ (𝜑 → (𝑇 ∈ dom 𝑈 ∧ (𝑈‘𝑇) = (𝑈‘𝑆))) |