Metamath Proof Explorer

Theorem ipoglblem

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

Ref Expression
Hypotheses ipolub.i ⊢ I = toInc ⁡ F
ipolub.f ⊢ φ → F ∈ V
ipolub.s ⊢ φ → S ⊆ F
ipoglblem.l ⊢ ≤ ˙ = ≤ I
Assertion ipoglblem ⊢ φ ∧ X ∈ F → X ⊆ ⋂ S ∧ ∀ z ∈ F z ⊆ ⋂ S → z ⊆ X ↔ ∀ y ∈ S X ≤ ˙ y ∧ ∀ z ∈ F ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ X

Proof

Step Hyp Ref Expression
1 ipolub.i ⊢ I = toInc ⁡ F
2 ipolub.f ⊢ φ → F ∈ V
3 ipolub.s ⊢ φ → S ⊆ F
4 ipoglblem.l ⊢ ≤ ˙ = ≤ I
5 ssint ⊢ X ⊆ ⋂ S ↔ ∀ y ∈ S X ⊆ y
6 2 ad2antrr ⊢ φ ∧ X ∈ F ∧ y ∈ S → F ∈ V
7 simplr ⊢ φ ∧ X ∈ F ∧ y ∈ S → X ∈ F
8 3 ad2antrr ⊢ φ ∧ X ∈ F ∧ y ∈ S → S ⊆ F
9 simpr ⊢ φ ∧ X ∈ F ∧ y ∈ S → y ∈ S
10 8 9 sseldd ⊢ φ ∧ X ∈ F ∧ y ∈ S → y ∈ F
11 1 4 ipole ⊢ F ∈ V ∧ X ∈ F ∧ y ∈ F → X ≤ ˙ y ↔ X ⊆ y
12 6 7 10 11 syl3anc ⊢ φ ∧ X ∈ F ∧ y ∈ S → X ≤ ˙ y ↔ X ⊆ y
13 12 ralbidva ⊢ φ ∧ X ∈ F → ∀ y ∈ S X ≤ ˙ y ↔ ∀ y ∈ S X ⊆ y
14 5 13 bitr4id ⊢ φ ∧ X ∈ F → X ⊆ ⋂ S ↔ ∀ y ∈ S X ≤ ˙ y
15 ssint ⊢ z ⊆ ⋂ S ↔ ∀ y ∈ S z ⊆ y
16 6 adantlr ⊢ φ ∧ X ∈ F ∧ z ∈ F ∧ y ∈ S → F ∈ V
17 simplr ⊢ φ ∧ X ∈ F ∧ z ∈ F ∧ y ∈ S → z ∈ F
18 10 adantlr ⊢ φ ∧ X ∈ F ∧ z ∈ F ∧ y ∈ S → y ∈ F
19 1 4 ipole ⊢ F ∈ V ∧ z ∈ F ∧ y ∈ F → z ≤ ˙ y ↔ z ⊆ y
20 16 17 18 19 syl3anc ⊢ φ ∧ X ∈ F ∧ z ∈ F ∧ y ∈ S → z ≤ ˙ y ↔ z ⊆ y
21 20 ralbidva ⊢ φ ∧ X ∈ F ∧ z ∈ F → ∀ y ∈ S z ≤ ˙ y ↔ ∀ y ∈ S z ⊆ y
22 15 21 bitr4id ⊢ φ ∧ X ∈ F ∧ z ∈ F → z ⊆ ⋂ S ↔ ∀ y ∈ S z ≤ ˙ y
23 2 ad2antrr ⊢ φ ∧ X ∈ F ∧ z ∈ F → F ∈ V
24 simpr ⊢ φ ∧ X ∈ F ∧ z ∈ F → z ∈ F
25 simplr ⊢ φ ∧ X ∈ F ∧ z ∈ F → X ∈ F
26 1 4 ipole ⊢ F ∈ V ∧ z ∈ F ∧ X ∈ F → z ≤ ˙ X ↔ z ⊆ X
27 23 24 25 26 syl3anc ⊢ φ ∧ X ∈ F ∧ z ∈ F → z ≤ ˙ X ↔ z ⊆ X
28 27 bicomd ⊢ φ ∧ X ∈ F ∧ z ∈ F → z ⊆ X ↔ z ≤ ˙ X
29 22 28 imbi12d ⊢ φ ∧ X ∈ F ∧ z ∈ F → z ⊆ ⋂ S → z ⊆ X ↔ ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ X
30 29 ralbidva ⊢ φ ∧ X ∈ F → ∀ z ∈ F z ⊆ ⋂ S → z ⊆ X ↔ ∀ z ∈ F ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ X
31 14 30 anbi12d ⊢ φ ∧ X ∈ F → X ⊆ ⋂ S ∧ ∀ z ∈ F z ⊆ ⋂ S → z ⊆ X ↔ ∀ y ∈ S X ≤ ˙ y ∧ ∀ z ∈ F ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ X