Theorem bj-prmoore 37602

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 37600). 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 463	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
2	1	adantrr 727	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
3		uniprg 4881	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
4	2, 3	syl 17	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
5		simprr 782	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐴 ⊆ 𝐵)
6		ssequn1 4138	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
7	5, 6	sylib 220	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∪ 𝐵) = 𝐵)
8	4, 7	eqtrd 2797	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = 𝐵)
9		prid2g 4720	. . . . 5 ⊢ (𝐵 ∈ V → 𝐵 ∈ {𝐴, 𝐵})
10	9	adantr 484	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ {𝐴, 𝐵})
11	8, 10	eqeltrd 2862	. . 3 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} ∈ {𝐴, 𝐵})
12		biid 263	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) ↔ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵))
13	12	bianass 652	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ↔ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵))
14		inteq 4908	. . . . . . . . . 10 ⊢ (𝑥 = {𝐴} → ∩ 𝑥 = ∩ {𝐴})
15		intsng 4941	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
16	15	adantl 485	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐴} = 𝐴)
17	14, 16	sylan9eqr 2819	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 = 𝐴)
18		prid1g 4719	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
19	18	adantl 485	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ {𝐴, 𝐵})
20	19	adantr 484	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → 𝐴 ∈ {𝐴, 𝐵})
21	17, 20	eqeltrd 2862	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
22	21	ex 416	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
23	22	adantr 484	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
24		inteq 4908	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐵} → ∩ 𝑥 = ∩ {𝐵})
25		intsng 4941	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ∩ {𝐵} = 𝐵)
26	25	adantr 484	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐵} = 𝐵)
27	24, 26	sylan9eqr 2819	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 = 𝐵)
28	9	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → 𝐵 ∈ {𝐴, 𝐵})
29	27, 28	eqeltrd 2862	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
30	29	ex 416	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
31	30	adantr 484	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
32		inteq 4908	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 = ∩ {𝐴, 𝐵})
33	32	adantl 485	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = ∩ {𝐴, 𝐵})
34	1	ad2antrr 736	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
35		intprg 4939	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
37		dfss2 3922	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
38	37	bilani 508	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∩ 𝐵) = 𝐴)
39	38	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∩ 𝐵) = 𝐴)
40	33, 36, 39	3eqtrd 2801	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = 𝐴)
41	18	ad3antlr 741	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → 𝐴 ∈ {𝐴, 𝐵})
42	40, 41	eqeltrd 2862	. . . . . . . 8 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
43	42	ex 416	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
44	31, 43	jaod 870	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
45	23, 44	jaod 870	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
46		sspr 4793	. . . . . 6 ⊢ (𝑥 ⊆ {𝐴, 𝐵} ↔ ((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
47		andir 1022	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) ↔ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)))
48		andir 1022	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)))
49		eqneqall 2968	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑥 ≠ ∅ → ⊥))
50	49	imp 410	. . . . . . . . . . 11 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ⊥)
51		simpl 486	. . . . . . . . . . 11 ⊢ ((𝑥 = {𝐴} ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
52	50, 51	orim12i 919	. . . . . . . . . 10 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → (⊥ ∨ 𝑥 = {𝐴}))
53		falim 1577	. . . . . . . . . . 11 ⊢ (⊥ → 𝑥 = {𝐴})
54	53	bj-jaoi1 37011	. . . . . . . . . 10 ⊢ ((⊥ ∨ 𝑥 = {𝐴}) → 𝑥 = {𝐴})
55	52, 54	syl 17	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → 𝑥 = {𝐴})
56	48, 55	sylbi 219	. . . . . . . 8 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
57		simpl 486	. . . . . . . 8 ⊢ (((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}))
58	56, 57	orim12i 919	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
59	47, 58	sylbi 219	. . . . . 6 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
60	46, 59	sylanb 590	. . . . 5 ⊢ ((𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
61	45, 60	impel 513	. . . 4 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
62	13, 61	sylanb 590	. . 3 ⊢ (((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ∧ (𝑥 ⊆ {𝐴, 𝐵} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ {𝐴, 𝐵})
63	11, 62	bj-ismooredr2 37597	. 2 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
64		pm3.22 463	. . . . 5 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
65	64	adantrr 727	. . . 4 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
66		prprc2 4725	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
67	66	adantl 485	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = {𝐴})
68	67	eqcomd 2768	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴} = {𝐴, 𝐵})
69	65, 68	syl 17	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} = {𝐴, 𝐵})
70		bj-snmoore 37600	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
71	70	ad2antrl 738	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} ∈ Moore)
72	69, 71	eqeltrrd 2863	. 2 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
73	63, 72	pm2.61ian 821	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 858   = wceq 1560  ⊥wfal 1572   ∈ wcel 2142   ≠ wne 2957  Vcvv 3454   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  {csn 4582  {cpr 4584  ∪ cuni 4865  ∩ cint 4905  Moorecmoore 37590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-pw 4557  df-sn 4583  df-pr 4585  df-uni 4866  df-int 4906  df-bj-moore 37591

This theorem is referenced by: (None)