Theorem bj-prmoore 35586

Description: A pair formed of two nested sets is a Moore collection. (Note that in the statement, if 𝐵 is a proper class, we are in the case of bj-snmoore 35584). A direct consequence is ⊢ {∅, 𝐴} ∈ Moore.

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

We also have the biconditional ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → ({𝐴, 𝐵} ∈ Moore ↔ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))). (Contributed by BJ, 11-Apr-2024.)

Assertion

Ref	Expression
bj-prmoore	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore)

Proof of Theorem bj-prmoore

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm3.22 460	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
2	1	adantrr 715	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
3		uniprg 4882	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
4	2, 3	syl 17	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
5		simprr 771	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐴 ⊆ 𝐵)
6		ssequn1 4140	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
7	5, 6	sylib 217	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∪ 𝐵) = 𝐵)
8	4, 7	eqtrd 2776	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = 𝐵)
9		prid2g 4722	. . . . 5 ⊢ (𝐵 ∈ V → 𝐵 ∈ {𝐴, 𝐵})
10	9	adantr 481	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ {𝐴, 𝐵})
11	8, 10	eqeltrd 2838	. . 3 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} ∈ {𝐴, 𝐵})
12		biid 260	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) ↔ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵))
13	12	bianass 640	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ↔ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵))
14		inteq 4910	. . . . . . . . . 10 ⊢ (𝑥 = {𝐴} → ∩ 𝑥 = ∩ {𝐴})
15		intsng 4946	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
16	15	adantl 482	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐴} = 𝐴)
17	14, 16	sylan9eqr 2798	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 = 𝐴)
18		prid1g 4721	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
19	18	adantl 482	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ {𝐴, 𝐵})
20	19	adantr 481	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → 𝐴 ∈ {𝐴, 𝐵})
21	17, 20	eqeltrd 2838	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
22	21	ex 413	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
23	22	adantr 481	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
24		inteq 4910	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐵} → ∩ 𝑥 = ∩ {𝐵})
25		intsng 4946	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ∩ {𝐵} = 𝐵)
26	25	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐵} = 𝐵)
27	24, 26	sylan9eqr 2798	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 = 𝐵)
28	9	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → 𝐵 ∈ {𝐴, 𝐵})
29	27, 28	eqeltrd 2838	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
30	29	ex 413	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
31	30	adantr 481	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
32		inteq 4910	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 = ∩ {𝐴, 𝐵})
33	32	adantl 482	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = ∩ {𝐴, 𝐵})
34	1	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
35		intprg 4942	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
37		df-ss 3927	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
38	37	biimpi 215	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
39	38	adantl 482	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∩ 𝐵) = 𝐴)
40	39	adantr 481	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∩ 𝐵) = 𝐴)
41	33, 36, 40	3eqtrd 2780	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = 𝐴)
42	18	ad3antlr 729	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → 𝐴 ∈ {𝐴, 𝐵})
43	41, 42	eqeltrd 2838	. . . . . . . 8 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
44	43	ex 413	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
45	31, 44	jaod 857	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
46	23, 45	jaod 857	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
47		sspr 4793	. . . . . 6 ⊢ (𝑥 ⊆ {𝐴, 𝐵} ↔ ((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
48		andir 1007	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) ↔ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)))
49		andir 1007	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)))
50		eqneqall 2954	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑥 ≠ ∅ → ⊥))
51	50	imp 407	. . . . . . . . . . 11 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ⊥)
52		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑥 = {𝐴} ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
53	51, 52	orim12i 907	. . . . . . . . . 10 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → (⊥ ∨ 𝑥 = {𝐴}))
54		falim 1558	. . . . . . . . . . 11 ⊢ (⊥ → 𝑥 = {𝐴})
55	54	bj-jaoi1 35035	. . . . . . . . . 10 ⊢ ((⊥ ∨ 𝑥 = {𝐴}) → 𝑥 = {𝐴})
56	53, 55	syl 17	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → 𝑥 = {𝐴})
57	49, 56	sylbi 216	. . . . . . . 8 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
58		simpl 483	. . . . . . . 8 ⊢ (((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}))
59	57, 58	orim12i 907	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
60	48, 59	sylbi 216	. . . . . 6 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
61	47, 60	sylanb 581	. . . . 5 ⊢ ((𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
62	46, 61	impel 506	. . . 4 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
63	13, 62	sylanb 581	. . 3 ⊢ (((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
64	11, 63	bj-ismooredr2 35581	. 2 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
65		pm3.22 460	. . . . 5 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
66	65	adantrr 715	. . . 4 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
67		prprc2 4727	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
68	67	adantl 482	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = {𝐴})
69	68	eqcomd 2742	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴} = {𝐴, 𝐵})
70	66, 69	syl 17	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} = {𝐴, 𝐵})
71		bj-snmoore 35584	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
72	71	ad2antrl 726	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} ∈ Moore)
73	70, 72	eqeltrrd 2839	. 2 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
74	64, 73	pm2.61ian 810	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 845   = wceq 1541  ⊥wfal 1553   ∈ wcel 2106   ≠ wne 2943  Vcvv 3445   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  {csn 4586  {cpr 4588  ∪ cuni 4865  ∩ cint 4907  Moorecmoore 35574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-pw 4562  df-sn 4587  df-pr 4589  df-uni 4866  df-int 4908  df-bj-moore 35575

This theorem is referenced by: (None)