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

Metamath Proof Explorer

Theorem ipolublem

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

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

Proof

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