This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lubeldm2d

Description: Member of the domain of the least upper bound function of a poset. (Contributed by Zhi Wang, 28-Sep-2024)

Ref Expression
Hypotheses lubeldm2d.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
lubeldm2d.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
lubeldm2d.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
lubeldm2d.p ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) )
lubeldm2d.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
Assertion lubeldm2d ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 lubeldm2d.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 lubeldm2d.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
3 lubeldm2d.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
4 lubeldm2d.p ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) )
5 lubeldm2d.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
9 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
10 6 7 8 9 5 lubeldm2 ⊢ ( 𝜑 → ( 𝑆 ∈ dom ( lub ‘ 𝐾 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ) )
11 3 dmeqd ⊢ ( 𝜑 → dom 𝑈 = dom ( lub ‘ 𝐾 ) )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ 𝑆 ∈ dom ( lub ‘ 𝐾 ) ) )
13 1 sseq2d ⊢ ( 𝜑 → ( 𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ ( Base ‘ 𝐾 ) ) )
14 2 breqd ⊢ ( 𝜑 → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
15 14 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
16 2 breqd ⊢ ( 𝜑 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) )
17 16 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 ) )
18 2 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑧 ) )
19 17 18 imbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
20 1 19 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
21 15 20 anbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
23 4 22 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
24 23 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ) )
25 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐾 ) ) )
26 25 anbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ) )
27 24 26 bitrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ) )
28 27 rexbidv2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
29 13 28 anbi12d ⊢ ( 𝜑 → ( ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ) )
30 10 12 29 3bitr4d ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃ 𝑥 ∈ 𝐵 𝜓 ) ) )