Theorem bj-prmoore 37116

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 37114). 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 459	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
2	1	adantrr 717	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
3		uniprg 4923	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
4	2, 3	syl 17	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
5		simprr 773	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐴 ⊆ 𝐵)
6		ssequn1 4186	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
7	5, 6	sylib 218	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∪ 𝐵) = 𝐵)
8	4, 7	eqtrd 2777	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = 𝐵)
9		prid2g 4761	. . . . 5 ⊢ (𝐵 ∈ V → 𝐵 ∈ {𝐴, 𝐵})
10	9	adantr 480	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ {𝐴, 𝐵})
11	8, 10	eqeltrd 2841	. . 3 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} ∈ {𝐴, 𝐵})
12		biid 261	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) ↔ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵))
13	12	bianass 642	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ↔ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵))
14		inteq 4949	. . . . . . . . . 10 ⊢ (𝑥 = {𝐴} → ∩ 𝑥 = ∩ {𝐴})
15		intsng 4983	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
16	15	adantl 481	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐴} = 𝐴)
17	14, 16	sylan9eqr 2799	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 = 𝐴)
18		prid1g 4760	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
19	18	adantl 481	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ {𝐴, 𝐵})
20	19	adantr 480	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → 𝐴 ∈ {𝐴, 𝐵})
21	17, 20	eqeltrd 2841	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
22	21	ex 412	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
23	22	adantr 480	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
24		inteq 4949	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐵} → ∩ 𝑥 = ∩ {𝐵})
25		intsng 4983	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ∩ {𝐵} = 𝐵)
26	25	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐵} = 𝐵)
27	24, 26	sylan9eqr 2799	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 = 𝐵)
28	9	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → 𝐵 ∈ {𝐴, 𝐵})
29	27, 28	eqeltrd 2841	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
30	29	ex 412	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
31	30	adantr 480	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
32		inteq 4949	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 = ∩ {𝐴, 𝐵})
33	32	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = ∩ {𝐴, 𝐵})
34	1	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
35		intprg 4981	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
37		dfss2 3969	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
38	37	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
39	38	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∩ 𝐵) = 𝐴)
40	39	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∩ 𝐵) = 𝐴)
41	33, 36, 40	3eqtrd 2781	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = 𝐴)
42	18	ad3antlr 731	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → 𝐴 ∈ {𝐴, 𝐵})
43	41, 42	eqeltrd 2841	. . . . . . . 8 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
44	43	ex 412	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
45	31, 44	jaod 860	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
46	23, 45	jaod 860	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
47		sspr 4835	. . . . . 6 ⊢ (𝑥 ⊆ {𝐴, 𝐵} ↔ ((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
48		andir 1011	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) ↔ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)))
49		andir 1011	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)))
50		eqneqall 2951	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑥 ≠ ∅ → ⊥))
51	50	imp 406	. . . . . . . . . . 11 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ⊥)
52		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 = {𝐴} ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
53	51, 52	orim12i 909	. . . . . . . . . 10 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → (⊥ ∨ 𝑥 = {𝐴}))
54		falim 1557	. . . . . . . . . . 11 ⊢ (⊥ → 𝑥 = {𝐴})
55	54	bj-jaoi1 36572	. . . . . . . . . 10 ⊢ ((⊥ ∨ 𝑥 = {𝐴}) → 𝑥 = {𝐴})
56	53, 55	syl 17	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → 𝑥 = {𝐴})
57	49, 56	sylbi 217	. . . . . . . 8 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
58		simpl 482	. . . . . . . 8 ⊢ (((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}))
59	57, 58	orim12i 909	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
60	48, 59	sylbi 217	. . . . . 6 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
61	47, 60	sylanb 581	. . . . 5 ⊢ ((𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
62	46, 61	impel 505	. . . 4 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
63	13, 62	sylanb 581	. . 3 ⊢ (((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
64	11, 63	bj-ismooredr2 37111	. 2 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
65		pm3.22 459	. . . . 5 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
66	65	adantrr 717	. . . 4 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
67		prprc2 4766	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
68	67	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = {𝐴})
69	68	eqcomd 2743	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴} = {𝐴, 𝐵})
70	66, 69	syl 17	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} = {𝐴, 𝐵})
71		bj-snmoore 37114	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
72	71	ad2antrl 728	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} ∈ Moore)
73	70, 72	eqeltrrd 2842	. 2 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
74	64, 73	pm2.61ian 812	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1540  ⊥wfal 1552   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  {csn 4626  {cpr 4628  ∪ cuni 4907  ∩ cint 4946  Moorecmoore 37104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-pw 4602  df-sn 4627  df-pr 4629  df-uni 4908  df-int 4947  df-bj-moore 37105

This theorem is referenced by: (None)