Metamath Proof Explorer

Theorem ipolublem

Description: Lemma for ipolubdm and ipolub . (Contributed by Zhi Wang, 28-Sep-2024)

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

Proof

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