Metamath Proof Explorer

Theorem lublecllem

Description: Lemma for lublecl and lubid . (Contributed by NM, 8-Sep-2018)

Ref Expression
Hypotheses lublecl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lublecl.l ⊢ ≤ = ( le ‘ 𝐾 )
lublecl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lublecl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
lublecl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion lublecllem ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ 𝑥 = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lublecl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lublecl.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lublecl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lublecl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 lublecl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ≤ 𝑋 ↔ 𝑧 ≤ 𝑋 ) )
7 6 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) )
8 6 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) )
9 8 imbi1i ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ↔ ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) )
10 9 ralbii ⊢ ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) )
11 7 10 anbi12i ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) ) )
12 1 2 posref ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
13 4 5 12 syl2anc ⊢ ( 𝜑 → 𝑋 ≤ 𝑋 )
14 breq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 ≤ 𝑋 ↔ 𝑋 ≤ 𝑋 ) )
15 breq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 ≤ 𝑥 ↔ 𝑋 ≤ 𝑥 ) )
16 14 15 imbi12d ⊢ ( 𝑧 = 𝑋 → ( ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ↔ ( 𝑋 ≤ 𝑋 → 𝑋 ≤ 𝑥 ) ) )
17 16 rspcva ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ) → ( 𝑋 ≤ 𝑋 → 𝑋 ≤ 𝑥 ) )
18 13 17 syl5com ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ) → 𝑋 ≤ 𝑥 ) )
19 5 18 mpand ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) → 𝑋 ≤ 𝑥 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) → 𝑋 ≤ 𝑥 ) )
21 idd ⊢ ( 𝑧 ∈ 𝐵 → ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑋 ) )
22 21 rgen ⊢ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑋 )
23 breq2 ⊢ ( 𝑤 = 𝑋 → ( 𝑧 ≤ 𝑤 ↔ 𝑧 ≤ 𝑋 ) )
24 23 imbi2d ⊢ ( 𝑤 = 𝑋 → ( ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) ↔ ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑋 ) ) )
25 24 ralbidv ⊢ ( 𝑤 = 𝑋 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑋 ) ) )
26 breq2 ⊢ ( 𝑤 = 𝑋 → ( 𝑥 ≤ 𝑤 ↔ 𝑥 ≤ 𝑋 ) )
27 25 26 imbi12d ⊢ ( 𝑤 = 𝑋 → ( ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) ↔ ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑋 ) → 𝑥 ≤ 𝑋 ) ) )
28 27 rspcv ⊢ ( 𝑋 ∈ 𝐵 → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑋 ) → 𝑥 ≤ 𝑋 ) ) )
29 5 28 syl ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑋 ) → 𝑥 ≤ 𝑋 ) ) )
30 22 29 mpii ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) → 𝑥 ≤ 𝑋 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) → 𝑥 ≤ 𝑋 ) )
32 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐾 ∈ Poset )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
34 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
35 1 2 posasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑋 ∧ 𝑋 ≤ 𝑥 ) ↔ 𝑥 = 𝑋 ) )
36 32 33 34 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑋 ∧ 𝑋 ≤ 𝑥 ) ↔ 𝑥 = 𝑋 ) )
37 36 biimpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑋 ∧ 𝑋 ≤ 𝑥 ) → 𝑥 = 𝑋 ) )
38 37 ancomsd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑥 ∧ 𝑥 ≤ 𝑋 ) → 𝑥 = 𝑋 ) )
39 20 31 38 syl2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) ) → 𝑥 = 𝑋 ) )
40 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑧 ≤ 𝑥 ↔ 𝑧 ≤ 𝑋 ) )
41 40 biimprd ⊢ ( 𝑥 = 𝑋 → ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) )
42 41 ralrimivw ⊢ ( 𝑥 = 𝑋 → ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) → ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) )
44 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑋 ∈ 𝐵 )
45 breq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 ≤ 𝑤 ↔ 𝑋 ≤ 𝑤 ) )
46 14 45 imbi12d ⊢ ( 𝑧 = 𝑋 → ( ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) ↔ ( 𝑋 ≤ 𝑋 → 𝑋 ≤ 𝑤 ) ) )
47 46 rspcva ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) ) → ( 𝑋 ≤ 𝑋 → 𝑋 ≤ 𝑤 ) )
48 pm5.5 ⊢ ( 𝑋 ≤ 𝑋 → ( ( 𝑋 ≤ 𝑋 → 𝑋 ≤ 𝑤 ) ↔ 𝑋 ≤ 𝑤 ) )
49 13 48 syl ⊢ ( 𝜑 → ( ( 𝑋 ≤ 𝑋 → 𝑋 ≤ 𝑤 ) ↔ 𝑋 ≤ 𝑤 ) )
50 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑤 ↔ 𝑋 ≤ 𝑤 ) )
51 50 bicomd ⊢ ( 𝑥 = 𝑋 → ( 𝑋 ≤ 𝑤 ↔ 𝑥 ≤ 𝑤 ) )
52 49 51 sylan9bb ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑋 ≤ 𝑋 → 𝑋 ≤ 𝑤 ) ↔ 𝑥 ≤ 𝑤 ) )
53 47 52 imbitrid ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) ) → 𝑥 ≤ 𝑤 ) )
54 44 53 mpand ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) )
55 54 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) )
56 55 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) → ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) )
57 43 56 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) ) )
58 57 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 = 𝑋 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) ) ) )
59 39 58 impbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑥 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ≤ 𝑋 → 𝑧 ≤ 𝑤 ) → 𝑥 ≤ 𝑤 ) ) ↔ 𝑥 = 𝑋 ) )
60 11 59 bitrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ 𝑥 = 𝑋 ) )