bj-prmoore

Description: A pair formed of two nested sets is a Moore collection. (Note that in the statement, if B is a proper class, we are in the case of bj-snmoore ). A direct consequence is |- { (/) , A } e. Moore_ .

More generally, any nonempty well-ordered chain of sets that is a set is a Moore collection.

We also have the biconditional |- ( ( A i^i B ) e. V -> ( { A , B } e. Moore_ <-> ( A C_ B \/ B C_ A ) ) ) . (Contributed by BJ, 11-Apr-2024)

		Ref	Expression
	Assertion	bj-prmoore	$⊢ (A \in V \land A \subseteq B) \to \{A, B\} \in \underline{Moore}$

Proof

Step	Hyp	Ref	Expression
1		pm3.22	$⊢ (B \in V \land A \in V) \to (A \in V \land B \in V)$
2	1	adantrr	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to (A \in V \land B \in V)$
3		uniprg	$⊢ (A \in V \land B \in V) \to ⋃ \{A, B\} = A \cup B$
4	2 3	syl	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to ⋃ \{A, B\} = A \cup B$
5		simprr	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to A \subseteq B$
6		ssequn1	$⊢ A \subseteq B \leftrightarrow A \cup B = B$
7	5 6	sylib	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to A \cup B = B$
8	4 7	eqtrd	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to ⋃ \{A, B\} = B$
9		prid2g	$⊢ B \in V \to B \in \{A, B\}$
10	9	adantr	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to B \in \{A, B\}$
11	8 10	eqeltrd	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to ⋃ \{A, B\} \in \{A, B\}$
12		biid	$⊢ (A \in V \land A \subseteq B) \leftrightarrow (A \in V \land A \subseteq B)$
13	12	bianass	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \leftrightarrow ((B \in V \land A \in V) \land A \subseteq B)$
14		inteq	$⊢ x = \{A\} \to ⋂ x = ⋂ \{A\}$
15		intsng	$⊢ A \in V \to ⋂ \{A\} = A$
16	15	adantl	$⊢ (B \in V \land A \in V) \to ⋂ \{A\} = A$
17	14 16	sylan9eqr	$⊢ ((B \in V \land A \in V) \land x = \{A\}) \to ⋂ x = A$
18		prid1g	$⊢ A \in V \to A \in \{A, B\}$
19	18	adantl	$⊢ (B \in V \land A \in V) \to A \in \{A, B\}$
20	19	adantr	$⊢ ((B \in V \land A \in V) \land x = \{A\}) \to A \in \{A, B\}$
21	17 20	eqeltrd	$⊢ ((B \in V \land A \in V) \land x = \{A\}) \to ⋂ x \in \{A, B\}$
22	21	ex	$⊢ (B \in V \land A \in V) \to (x = \{A\} \to ⋂ x \in \{A, B\})$
23	22	adantr	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to (x = \{A\} \to ⋂ x \in \{A, B\})$
24		inteq	$⊢ x = \{B\} \to ⋂ x = ⋂ \{B\}$
25		intsng	$⊢ B \in V \to ⋂ \{B\} = B$
26	25	adantr	$⊢ (B \in V \land A \in V) \to ⋂ \{B\} = B$
27	24 26	sylan9eqr	$⊢ ((B \in V \land A \in V) \land x = \{B\}) \to ⋂ x = B$
28	9	ad2antrr	$⊢ ((B \in V \land A \in V) \land x = \{B\}) \to B \in \{A, B\}$
29	27 28	eqeltrd	$⊢ ((B \in V \land A \in V) \land x = \{B\}) \to ⋂ x \in \{A, B\}$
30	29	ex	$⊢ (B \in V \land A \in V) \to (x = \{B\} \to ⋂ x \in \{A, B\})$
31	30	adantr	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to (x = \{B\} \to ⋂ x \in \{A, B\})$
32		inteq	$⊢ x = \{A, B\} \to ⋂ x = ⋂ \{A, B\}$
33	32	adantl	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to ⋂ x = ⋂ \{A, B\}$
34	1	ad2antrr	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to (A \in V \land B \in V)$
35		intprg	$⊢ (A \in V \land B \in V) \to ⋂ \{A, B\} = A \cap B$
36	34 35	syl	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to ⋂ \{A, B\} = A \cap B$
37		dfss2	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
38	37	bilani	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to A \cap B = A$
39	38	adantr	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to A \cap B = A$
40	33 36 39	3eqtrd	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to ⋂ x = A$
41	18	ad3antlr	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to A \in \{A, B\}$
42	40 41	eqeltrd	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to ⋂ x \in \{A, B\}$
43	42	ex	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to (x = \{A, B\} \to ⋂ x \in \{A, B\})$
44	31 43	jaod	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to ((x = \{B\} \lor x = \{A, B\}) \to ⋂ x \in \{A, B\})$
45	23 44	jaod	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to ((x = \{A\} \lor (x = \{B\} \lor x = \{A, B\})) \to ⋂ x \in \{A, B\})$
46		sspr	$⊢ x \subseteq \{A, B\} \leftrightarrow ((x = \emptyset \lor x = \{A\}) \lor (x = \{B\} \lor x = \{A, B\}))$
47		andir	$⊢ (((x = \emptyset \lor x = \{A\}) \lor (x = \{B\} \lor x = \{A, B\})) \land x \neq \emptyset) \leftrightarrow (((x = \emptyset \lor x = \{A\}) \land x \neq \emptyset) \lor ((x = \{B\} \lor x = \{A, B\}) \land x \neq \emptyset))$
48		andir	$⊢ ((x = \emptyset \lor x = \{A\}) \land x \neq \emptyset) \leftrightarrow ((x = \emptyset \land x \neq \emptyset) \lor (x = \{A\} \land x \neq \emptyset))$
49		eqneqall	$⊢ x = \emptyset \to (x \neq \emptyset \to ⊥)$
50	49	imp	$⊢ (x = \emptyset \land x \neq \emptyset) \to ⊥$
51		simpl	$⊢ (x = \{A\} \land x \neq \emptyset) \to x = \{A\}$
52	50 51	orim12i	$⊢ ((x = \emptyset \land x \neq \emptyset) \lor (x = \{A\} \land x \neq \emptyset)) \to (⊥ \lor x = \{A\})$
53		falim	$⊢ ⊥ \to x = \{A\}$
54	53	bj-jaoi1	$⊢ (⊥ \lor x = \{A\}) \to x = \{A\}$
55	52 54	syl	$⊢ ((x = \emptyset \land x \neq \emptyset) \lor (x = \{A\} \land x \neq \emptyset)) \to x = \{A\}$
56	48 55	sylbi	$⊢ ((x = \emptyset \lor x = \{A\}) \land x \neq \emptyset) \to x = \{A\}$
57		simpl	$⊢ ((x = \{B\} \lor x = \{A, B\}) \land x \neq \emptyset) \to (x = \{B\} \lor x = \{A, B\})$
58	56 57	orim12i	$⊢ (((x = \emptyset \lor x = \{A\}) \land x \neq \emptyset) \lor ((x = \{B\} \lor x = \{A, B\}) \land x \neq \emptyset)) \to (x = \{A\} \lor (x = \{B\} \lor x = \{A, B\}))$
59	47 58	sylbi	$⊢ (((x = \emptyset \lor x = \{A\}) \lor (x = \{B\} \lor x = \{A, B\})) \land x \neq \emptyset) \to (x = \{A\} \lor (x = \{B\} \lor x = \{A, B\}))$
60	46 59	sylanb	$⊢ (x \subseteq \{A, B\} \land x \neq \emptyset) \to (x = \{A\} \lor (x = \{B\} \lor x = \{A, B\}))$
61	45 60	impel	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land (x \subseteq \{A, B\} \land x \neq \emptyset)) \to ⋂ x \in \{A, B\}$
62	13 61	sylanb	$⊢ ((B \in V \land (A \in V \land A \subseteq B)) \land (x \subseteq \{A, B\} \land x \neq \emptyset)) \to ⋂ x \in \{A, B\}$
63	11 62	bj-ismooredr2	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to \{A, B\} \in \underline{Moore}$
64		pm3.22	$⊢ (\neg B \in V \land A \in V) \to (A \in V \land \neg B \in V)$
65	64	adantrr	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to (A \in V \land \neg B \in V)$
66		prprc2	$⊢ \neg B \in V \to \{A, B\} = \{A\}$
67	66	adantl	$⊢ (A \in V \land \neg B \in V) \to \{A, B\} = \{A\}$
68	67	eqcomd	$⊢ (A \in V \land \neg B \in V) \to \{A\} = \{A, B\}$
69	65 68	syl	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to \{A\} = \{A, B\}$
70		bj-snmoore	$⊢ A \in V \to \{A\} \in \underline{Moore}$
71	70	ad2antrl	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to \{A\} \in \underline{Moore}$
72	69 71	eqeltrrd	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to \{A, B\} \in \underline{Moore}$
73	63 72	pm2.61ian	$⊢ (A \in V \land A \subseteq B) \to \{A, B\} \in \underline{Moore}$

Metamath Proof Explorer

Theorem bj-prmoore

Proof