ipolublem

	Ref	Expression
Hypotheses	ipolub.i	$⊢ I = toInc (F)$
	ipolub.f	$⊢ φ \to F \in V$
	ipolub.s	$⊢ φ \to S \subseteq F$
	ipolublem.l	$⊢ \underset{˙}{\leq} = \leq_{I}$
Assertion	ipolublem	$⊢ (φ \land X \in F) \to ((⋃ S \subseteq X \land \forall z \in F (⋃ S \subseteq z \to X \subseteq z)) \leftrightarrow (\forall y \in S y \underset{˙}{\leq} X \land \forall z \in F (\forall y \in S y \underset{˙}{\leq} z \to X \underset{˙}{\leq} z)))$

Proof

Step	Hyp	Ref	Expression
1		ipolub.i	$⊢ I = toInc (F)$
2		ipolub.f	$⊢ φ \to F \in V$
3		ipolub.s	$⊢ φ \to S \subseteq F$
4		ipolublem.l	$⊢ \underset{˙}{\leq} = \leq_{I}$
5		unissb	$⊢ ⋃ S \subseteq X \leftrightarrow \forall y \in S y \subseteq X$
6	2	ad2antrr	$⊢ ((φ \land X \in F) \land y \in S) \to F \in V$
7	3	ad2antrr	$⊢ ((φ \land X \in F) \land y \in S) \to S \subseteq F$
8		simpr	$⊢ ((φ \land X \in F) \land y \in S) \to y \in S$
9	7 8	sseldd	$⊢ ((φ \land X \in F) \land y \in S) \to y \in F$
10		simplr	$⊢ ((φ \land X \in F) \land y \in S) \to X \in F$
11	1 4	ipole	$⊢ (F \in V \land y \in F \land X \in F) \to (y \underset{˙}{\leq} X \leftrightarrow y \subseteq X)$
12	6 9 10 11	syl3anc	$⊢ ((φ \land X \in F) \land y \in S) \to (y \underset{˙}{\leq} X \leftrightarrow y \subseteq X)$
13	12	ralbidva	$⊢ (φ \land X \in F) \to (\forall y \in S y \underset{˙}{\leq} X \leftrightarrow \forall y \in S y \subseteq X)$
14	5 13	bitr4id	$⊢ (φ \land X \in F) \to (⋃ S \subseteq X \leftrightarrow \forall y \in S y \underset{˙}{\leq} X)$
15		unissb	$⊢ ⋃ S \subseteq z \leftrightarrow \forall y \in S y \subseteq z$
16	6	adantlr	$⊢ (((φ \land X \in F) \land z \in F) \land y \in S) \to F \in V$
17	9	adantlr	$⊢ (((φ \land X \in F) \land z \in F) \land y \in S) \to y \in F$
18		simplr	$⊢ (((φ \land X \in F) \land z \in F) \land y \in S) \to z \in F$
19	1 4	ipole	$⊢ (F \in V \land y \in F \land z \in F) \to (y \underset{˙}{\leq} z \leftrightarrow y \subseteq z)$
20	16 17 18 19	syl3anc	$⊢ (((φ \land X \in F) \land z \in F) \land y \in S) \to (y \underset{˙}{\leq} z \leftrightarrow y \subseteq z)$
21	20	ralbidva	$⊢ ((φ \land X \in F) \land z \in F) \to (\forall y \in S y \underset{˙}{\leq} z \leftrightarrow \forall y \in S y \subseteq z)$
22	15 21	bitr4id	$⊢ ((φ \land X \in F) \land z \in F) \to (⋃ S \subseteq z \leftrightarrow \forall y \in S y \underset{˙}{\leq} z)$
23	2	ad2antrr	$⊢ ((φ \land X \in F) \land z \in F) \to F \in V$
24		simplr	$⊢ ((φ \land X \in F) \land z \in F) \to X \in F$
25		simpr	$⊢ ((φ \land X \in F) \land z \in F) \to z \in F$
26	1 4	ipole	$⊢ (F \in V \land X \in F \land z \in F) \to (X \underset{˙}{\leq} z \leftrightarrow X \subseteq z)$
27	23 24 25 26	syl3anc	$⊢ ((φ \land X \in F) \land z \in F) \to (X \underset{˙}{\leq} z \leftrightarrow X \subseteq z)$
28	27	bicomd	$⊢ ((φ \land X \in F) \land z \in F) \to (X \subseteq z \leftrightarrow X \underset{˙}{\leq} z)$
29	22 28	imbi12d	$⊢ ((φ \land X \in F) \land z \in F) \to ((⋃ S \subseteq z \to X \subseteq z) \leftrightarrow (\forall y \in S y \underset{˙}{\leq} z \to X \underset{˙}{\leq} z))$
30	29	ralbidva	$⊢ (φ \land X \in F) \to (\forall z \in F (⋃ S \subseteq z \to X \subseteq z) \leftrightarrow \forall z \in F (\forall y \in S y \underset{˙}{\leq} z \to X \underset{˙}{\leq} z))$
31	14 30	anbi12d	$⊢ (φ \land X \in F) \to ((⋃ S \subseteq X \land \forall z \in F (⋃ S \subseteq z \to X \subseteq z)) \leftrightarrow (\forall y \in S y \underset{˙}{\leq} X \land \forall z \in F (\forall y \in S y \underset{˙}{\leq} z \to X \underset{˙}{\leq} z)))$

Metamath Proof Explorer

Theorem ipolublem

Proof