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		df-ss	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
38	37	biimpi	$⊢ A \subseteq B \to A \cap B = A$
39	38	adantl	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to A \cap B = A$
40	39	adantr	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to A \cap B = A$
41	33 36 40	3eqtrd	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to ⋂ x = A$
42	18	ad3antlr	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to A \in \{A, B\}$
43	41 42	eqeltrd	$⊢ (((B \in V \land A \in V) \land A \subseteq B) \land x = \{A, B\}) \to ⋂ x \in \{A, B\}$
44	43	ex	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to (x = \{A, B\} \to ⋂ x \in \{A, B\})$
45	31 44	jaod	$⊢ ((B \in V \land A \in V) \land A \subseteq B) \to ((x = \{B\} \lor x = \{A, B\}) \to ⋂ x \in \{A, B\})$
46	23 45	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\})$
47		sspr	$⊢ x \subseteq \{A, B\} \leftrightarrow ((x = \emptyset \lor x = \{A\}) \lor (x = \{B\} \lor x = \{A, B\}))$
48		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))$
49		andir	$⊢ ((x = \emptyset \lor x = \{A\}) \land x \neq \emptyset) \leftrightarrow ((x = \emptyset \land x \neq \emptyset) \lor (x = \{A\} \land x \neq \emptyset))$
50		eqneqall	$⊢ x = \emptyset \to (x \neq \emptyset \to ⊥)$
51	50	imp	$⊢ (x = \emptyset \land x \neq \emptyset) \to ⊥$
52		simpl	$⊢ (x = \{A\} \land x \neq \emptyset) \to x = \{A\}$
53	51 52	orim12i	$⊢ ((x = \emptyset \land x \neq \emptyset) \lor (x = \{A\} \land x \neq \emptyset)) \to (⊥ \lor x = \{A\})$
54		falim	$⊢ ⊥ \to x = \{A\}$
55	54	bj-jaoi1	$⊢ (⊥ \lor x = \{A\}) \to x = \{A\}$
56	53 55	syl	$⊢ ((x = \emptyset \land x \neq \emptyset) \lor (x = \{A\} \land x \neq \emptyset)) \to x = \{A\}$
57	49 56	sylbi	$⊢ ((x = \emptyset \lor x = \{A\}) \land x \neq \emptyset) \to x = \{A\}$
58		simpl	$⊢ ((x = \{B\} \lor x = \{A, B\}) \land x \neq \emptyset) \to (x = \{B\} \lor x = \{A, B\})$
59	57 58	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\}))$
60	48 59	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\}))$
61	47 60	sylanb	$⊢ (x \subseteq \{A, B\} \land x \neq \emptyset) \to (x = \{A\} \lor (x = \{B\} \lor x = \{A, B\}))$
62	46 61	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\}$
63	13 62	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\}$
64	11 63	bj-ismooredr2	$⊢ (B \in V \land (A \in V \land A \subseteq B)) \to \{A, B\} \in \underline{Moore}$
65		pm3.22	$⊢ (\neg B \in V \land A \in V) \to (A \in V \land \neg B \in V)$
66	65	adantrr	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to (A \in V \land \neg B \in V)$
67		prprc2	$⊢ \neg B \in V \to \{A, B\} = \{A\}$
68	67	adantl	$⊢ (A \in V \land \neg B \in V) \to \{A, B\} = \{A\}$
69	68	eqcomd	$⊢ (A \in V \land \neg B \in V) \to \{A\} = \{A, B\}$
70	66 69	syl	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to \{A\} = \{A, B\}$
71		bj-snmoore	$⊢ A \in V \to \{A\} \in \underline{Moore}$
72	71	ad2antrl	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to \{A\} \in \underline{Moore}$
73	70 72	eqeltrrd	$⊢ (\neg B \in V \land (A \in V \land A \subseteq B)) \to \{A, B\} \in \underline{Moore}$
74	64 73	pm2.61ian	$⊢ (A \in V \land A \subseteq B) \to \{A, B\} \in \underline{Moore}$

Metamath Proof Explorer

Theorem bj-prmoore

Proof