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

Metamath Proof Explorer

Theorem ipoglblem

Description: Lemma for ipoglbdm and ipoglb . (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Hypotheses ipolub.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
ipolub.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
ipolub.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
ipoglblem.l ⊢ ≤ = ( le ‘ 𝐼 )
Assertion ipoglblem ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) → ( ( 𝑋 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 ipolub.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
2 ipolub.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3 ipolub.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
4 ipoglblem.l ⊢ ≤ = ( le ‘ 𝐼 )
5 ssint ⊢ ( 𝑋 ⊆ ∩ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 𝑋 ⊆ 𝑦 )
6 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐹 ∈ 𝑉 )
7 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑋 ∈ 𝐹 )
8 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ⊆ 𝐹 )
9 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
10 8 9 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐹 )
11 1 4 ipole ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑋 ≤ 𝑦 ↔ 𝑋 ⊆ 𝑦 ) )
12 6 7 10 11 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑋 ≤ 𝑦 ↔ 𝑋 ⊆ 𝑦 ) )
13 12 ralbidva ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) → ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑋 ⊆ 𝑦 ) )
14 5 13 bitr4id ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) → ( 𝑋 ⊆ ∩ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ) )
15 ssint ⊢ ( 𝑧 ⊆ ∩ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 )
16 6 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐹 ∈ 𝑉 )
17 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑧 ∈ 𝐹 )
18 10 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐹 )
19 1 4 ipole ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑧 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑧 ≤ 𝑦 ↔ 𝑧 ⊆ 𝑦 ) )
20 16 17 18 19 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑧 ≤ 𝑦 ↔ 𝑧 ⊆ 𝑦 ) )
21 20 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ⊆ 𝑦 ) )
22 15 21 bitr4id ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → ( 𝑧 ⊆ ∩ 𝑆 ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ) )
23 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → 𝐹 ∈ 𝑉 )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → 𝑧 ∈ 𝐹 )
25 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → 𝑋 ∈ 𝐹 )
26 1 4 ipole ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑧 ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) → ( 𝑧 ≤ 𝑋 ↔ 𝑧 ⊆ 𝑋 ) )
27 23 24 25 26 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → ( 𝑧 ≤ 𝑋 ↔ 𝑧 ⊆ 𝑋 ) )
28 27 bicomd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → ( 𝑧 ⊆ 𝑋 ↔ 𝑧 ≤ 𝑋 ) )
29 22 28 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝐹 ) → ( ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋 ) ) )
30 29 ralbidva ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋 ) ) )
31 14 30 anbi12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐹 ) → ( ( 𝑋 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑋 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑋 ) ) ) )