ipodrsfi

Description: Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015)

		Ref	Expression
	Assertion	ipodrsfi	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to \exists z \in A ⋃ X \subseteq z$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to X \subseteq A$
2		ipodrscl	$⊢ toInc (A) \in Dirset \to A \in V$
3		eqid	$⊢ toInc (A) = toInc (A)$
4	3	ipobas	$⊢ A \in V \to A = {Base}_{toInc (A)}$
5	2 4	syl	$⊢ toInc (A) \in Dirset \to A = {Base}_{toInc (A)}$
6	5	3ad2ant1	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to A = {Base}_{toInc (A)}$
7	1 6	sseqtrd	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to X \subseteq {Base}_{toInc (A)}$
8		eqid	$⊢ {Base}_{toInc (A)} = {Base}_{toInc (A)}$
9		eqid	$⊢ \leq_{toInc (A)} = \leq_{toInc (A)}$
10	8 9	drsdirfi	$⊢ (toInc (A) \in Dirset \land X \subseteq {Base}_{toInc (A)} \land X \in Fin) \to \exists z \in {Base}_{toInc (A)} \forall w \in X w \leq_{toInc (A)} z$
11	7 10	syld3an2	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to \exists z \in {Base}_{toInc (A)} \forall w \in X w \leq_{toInc (A)} z$
12	6	rexeqdv	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to (\exists z \in A \forall w \in X w \leq_{toInc (A)} z \leftrightarrow \exists z \in {Base}_{toInc (A)} \forall w \in X w \leq_{toInc (A)} z)$
13	2	3ad2ant1	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to A \in V$
14	13	adantr	$⊢ ((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land (z \in A \land w \in X)) \to A \in V$
15	1	sselda	$⊢ ((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land w \in X) \to w \in A$
16	15	adantrl	$⊢ ((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land (z \in A \land w \in X)) \to w \in A$
17		simprl	$⊢ ((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land (z \in A \land w \in X)) \to z \in A$
18	3 9	ipole	$⊢ (A \in V \land w \in A \land z \in A) \to (w \leq_{toInc (A)} z \leftrightarrow w \subseteq z)$
19	14 16 17 18	syl3anc	$⊢ ((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land (z \in A \land w \in X)) \to (w \leq_{toInc (A)} z \leftrightarrow w \subseteq z)$
20	19	anassrs	$⊢ (((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land z \in A) \land w \in X) \to (w \leq_{toInc (A)} z \leftrightarrow w \subseteq z)$
21	20	ralbidva	$⊢ ((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land z \in A) \to (\forall w \in X w \leq_{toInc (A)} z \leftrightarrow \forall w \in X w \subseteq z)$
22		unissb	$⊢ ⋃ X \subseteq z \leftrightarrow \forall w \in X w \subseteq z$
23	21 22	bitr4di	$⊢ ((toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \land z \in A) \to (\forall w \in X w \leq_{toInc (A)} z \leftrightarrow ⋃ X \subseteq z)$
24	23	rexbidva	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to (\exists z \in A \forall w \in X w \leq_{toInc (A)} z \leftrightarrow \exists z \in A ⋃ X \subseteq z)$
25	12 24	bitr3d	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to (\exists z \in {Base}_{toInc (A)} \forall w \in X w \leq_{toInc (A)} z \leftrightarrow \exists z \in A ⋃ X \subseteq z)$
26	11 25	mpbid	$⊢ (toInc (A) \in Dirset \land X \subseteq A \land X \in Fin) \to \exists z \in A ⋃ X \subseteq z$

Metamath Proof Explorer

Theorem ipodrsfi

Proof