Theorem bj-prmoore 35996

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 35994). 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 461	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
2	1	adantrr 716	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
3		uniprg 4926	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
4	2, 3	syl 17	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
5		simprr 772	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐴 ⊆ 𝐵)
6		ssequn1 4181	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
7	5, 6	sylib 217	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∪ 𝐵) = 𝐵)
8	4, 7	eqtrd 2773	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = 𝐵)
9		prid2g 4766	. . . . 5 ⊢ (𝐵 ∈ V → 𝐵 ∈ {𝐴, 𝐵})
10	9	adantr 482	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ {𝐴, 𝐵})
11	8, 10	eqeltrd 2834	. . 3 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} ∈ {𝐴, 𝐵})
12		biid 261	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) ↔ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵))
13	12	bianass 641	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ↔ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵))
14		inteq 4954	. . . . . . . . . 10 ⊢ (𝑥 = {𝐴} → ∩ 𝑥 = ∩ {𝐴})
15		intsng 4990	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
16	15	adantl 483	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐴} = 𝐴)
17	14, 16	sylan9eqr 2795	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 = 𝐴)
18		prid1g 4765	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
19	18	adantl 483	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ {𝐴, 𝐵})
20	19	adantr 482	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → 𝐴 ∈ {𝐴, 𝐵})
21	17, 20	eqeltrd 2834	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
22	21	ex 414	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
23	22	adantr 482	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
24		inteq 4954	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐵} → ∩ 𝑥 = ∩ {𝐵})
25		intsng 4990	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ∩ {𝐵} = 𝐵)
26	25	adantr 482	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐵} = 𝐵)
27	24, 26	sylan9eqr 2795	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 = 𝐵)
28	9	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → 𝐵 ∈ {𝐴, 𝐵})
29	27, 28	eqeltrd 2834	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
30	29	ex 414	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
31	30	adantr 482	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
32		inteq 4954	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 = ∩ {𝐴, 𝐵})
33	32	adantl 483	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = ∩ {𝐴, 𝐵})
34	1	ad2antrr 725	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
35		intprg 4986	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
37		df-ss 3966	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
38	37	biimpi 215	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
39	38	adantl 483	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∩ 𝐵) = 𝐴)
40	39	adantr 482	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∩ 𝐵) = 𝐴)
41	33, 36, 40	3eqtrd 2777	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = 𝐴)
42	18	ad3antlr 730	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → 𝐴 ∈ {𝐴, 𝐵})
43	41, 42	eqeltrd 2834	. . . . . . . 8 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
44	43	ex 414	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
45	31, 44	jaod 858	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
46	23, 45	jaod 858	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
47		sspr 4837	. . . . . 6 ⊢ (𝑥 ⊆ {𝐴, 𝐵} ↔ ((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
48		andir 1008	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) ↔ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)))
49		andir 1008	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)))
50		eqneqall 2952	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑥 ≠ ∅ → ⊥))
51	50	imp 408	. . . . . . . . . . 11 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ⊥)
52		simpl 484	. . . . . . . . . . 11 ⊢ ((𝑥 = {𝐴} ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
53	51, 52	orim12i 908	. . . . . . . . . 10 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → (⊥ ∨ 𝑥 = {𝐴}))
54		falim 1559	. . . . . . . . . . 11 ⊢ (⊥ → 𝑥 = {𝐴})
55	54	bj-jaoi1 35448	. . . . . . . . . 10 ⊢ ((⊥ ∨ 𝑥 = {𝐴}) → 𝑥 = {𝐴})
56	53, 55	syl 17	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → 𝑥 = {𝐴})
57	49, 56	sylbi 216	. . . . . . . 8 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
58		simpl 484	. . . . . . . 8 ⊢ (((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}))
59	57, 58	orim12i 908	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
60	48, 59	sylbi 216	. . . . . 6 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
61	47, 60	sylanb 582	. . . . 5 ⊢ ((𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
62	46, 61	impel 507	. . . 4 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
63	13, 62	sylanb 582	. . 3 ⊢ (((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
64	11, 63	bj-ismooredr2 35991	. 2 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
65		pm3.22 461	. . . . 5 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
66	65	adantrr 716	. . . 4 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
67		prprc2 4771	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
68	67	adantl 483	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = {𝐴})
69	68	eqcomd 2739	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴} = {𝐴, 𝐵})
70	66, 69	syl 17	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} = {𝐴, 𝐵})
71		bj-snmoore 35994	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
72	71	ad2antrl 727	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} ∈ Moore)
73	70, 72	eqeltrrd 2835	. 2 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
74	64, 73	pm2.61ian 811	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 846   = wceq 1542  ⊥wfal 1554   ∈ wcel 2107   ≠ wne 2941  Vcvv 3475   ∪ cun 3947   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  {csn 4629  {cpr 4631  ∪ cuni 4909  ∩ cint 4951  Moorecmoore 35984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-pw 4605  df-sn 4630  df-pr 4632  df-uni 4910  df-int 4952  df-bj-moore 35985

This theorem is referenced by: (None)