isipodrs

Description: Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015)

		Ref	Expression
	Assertion	isipodrs	$⊢ toInc (A) \in Dirset \leftrightarrow (A \in V \land A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{toInc (A)} = {Base}_{toInc (A)}$
2	1	drsbn0	$⊢ toInc (A) \in Dirset \to {Base}_{toInc (A)} \neq \emptyset$
3	2	neneqd	$⊢ toInc (A) \in Dirset \to \neg {Base}_{toInc (A)} = \emptyset$
4		fvprc	$⊢ \neg A \in V \to toInc (A) = \emptyset$
5	4	fveq2d	$⊢ \neg A \in V \to {Base}_{toInc (A)} = {Base}_{\emptyset}$
6		base0	$⊢ \emptyset = {Base}_{\emptyset}$
7	5 6	eqtr4di	$⊢ \neg A \in V \to {Base}_{toInc (A)} = \emptyset$
8	3 7	nsyl2	$⊢ toInc (A) \in Dirset \to A \in V$
9		simp1	$⊢ (A \in V \land A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z) \to A \in V$
10		eqid	$⊢ \leq_{toInc (A)} = \leq_{toInc (A)}$
11	1 10	isdrs	$⊢ toInc (A) \in Dirset \leftrightarrow (toInc (A) \in Proset \land {Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z))$
12		eqid	$⊢ toInc (A) = toInc (A)$
13	12	ipopos	$⊢ toInc (A) \in Poset$
14		posprs	$⊢ toInc (A) \in Poset \to toInc (A) \in Proset$
15	13 14	mp1i	$⊢ A \in V \to toInc (A) \in Proset$
16		id	$⊢ A \in V \to A \in V$
17	15 16	2thd	$⊢ A \in V \to (toInc (A) \in Proset \leftrightarrow A \in V)$
18	12	ipobas	$⊢ A \in V \to A = {Base}_{toInc (A)}$
19		neeq1	$⊢ A = {Base}_{toInc (A)} \to (A \neq \emptyset \leftrightarrow {Base}_{toInc (A)} \neq \emptyset)$
20		rexeq	$⊢ A = {Base}_{toInc (A)} \to (\exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z) \leftrightarrow \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z))$
21	20	raleqbi1dv	$⊢ A = {Base}_{toInc (A)} \to (\forall y \in A \exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z) \leftrightarrow \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z))$
22	21	raleqbi1dv	$⊢ A = {Base}_{toInc (A)} \to (\forall x \in A \forall y \in A \exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z) \leftrightarrow \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z))$
23	19 22	anbi12d	$⊢ A = {Base}_{toInc (A)} \to ((A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)) \leftrightarrow ({Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)))$
24	18 23	syl	$⊢ A \in V \to ((A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)) \leftrightarrow ({Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)))$
25		simpll	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to A \in V$
26		simplrl	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to x \in A$
27		simpr	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to z \in A$
28	12 10	ipole	$⊢ (A \in V \land x \in A \land z \in A) \to (x \leq_{toInc (A)} z \leftrightarrow x \subseteq z)$
29	25 26 27 28	syl3anc	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to (x \leq_{toInc (A)} z \leftrightarrow x \subseteq z)$
30		simplrr	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to y \in A$
31	12 10	ipole	$⊢ (A \in V \land y \in A \land z \in A) \to (y \leq_{toInc (A)} z \leftrightarrow y \subseteq z)$
32	25 30 27 31	syl3anc	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to (y \leq_{toInc (A)} z \leftrightarrow y \subseteq z)$
33	29 32	anbi12d	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to ((x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z) \leftrightarrow (x \subseteq z \land y \subseteq z))$
34		unss	$⊢ (x \subseteq z \land y \subseteq z) \leftrightarrow x \cup y \subseteq z$
35	33 34	bitrdi	$⊢ ((A \in V \land (x \in A \land y \in A)) \land z \in A) \to ((x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z) \leftrightarrow x \cup y \subseteq z)$
36	35	rexbidva	$⊢ (A \in V \land (x \in A \land y \in A)) \to (\exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z) \leftrightarrow \exists z \in A x \cup y \subseteq z)$
37	36	2ralbidva	$⊢ A \in V \to (\forall x \in A \forall y \in A \exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z) \leftrightarrow \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z)$
38	37	anbi2d	$⊢ A \in V \to ((A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)) \leftrightarrow (A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z))$
39	24 38	bitr3d	$⊢ A \in V \to (({Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)) \leftrightarrow (A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z))$
40	17 39	anbi12d	$⊢ A \in V \to ((toInc (A) \in Proset \land ({Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z))) \leftrightarrow (A \in V \land (A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z)))$
41		3anass	$⊢ (toInc (A) \in Proset \land {Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)) \leftrightarrow (toInc (A) \in Proset \land ({Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)))$
42		3anass	$⊢ (A \in V \land A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z) \leftrightarrow (A \in V \land (A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z))$
43	40 41 42	3bitr4g	$⊢ A \in V \to ((toInc (A) \in Proset \land {Base}_{toInc (A)} \neq \emptyset \land \forall x \in {Base}_{toInc (A)} \forall y \in {Base}_{toInc (A)} \exists z \in {Base}_{toInc (A)} (x \leq_{toInc (A)} z \land y \leq_{toInc (A)} z)) \leftrightarrow (A \in V \land A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z))$
44	11 43	bitrid	$⊢ A \in V \to (toInc (A) \in Dirset \leftrightarrow (A \in V \land A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z))$
45	8 9 44	pm5.21nii	$⊢ toInc (A) \in Dirset \leftrightarrow (A \in V \land A \neq \emptyset \land \forall x \in A \forall y \in A \exists z \in A x \cup y \subseteq z)$

Metamath Proof Explorer

Theorem isipodrs

Proof