Theorem bj-prmoore 37103

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 37101). 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 4887	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
4	2, 3	syl 17	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = (𝐴 ∪ 𝐵))
5		simprr 772	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐴 ⊆ 𝐵)
6		ssequn1 4149	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
7	5, 6	sylib 218	. . . . 5 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∪ 𝐵) = 𝐵)
8	4, 7	eqtrd 2764	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} = 𝐵)
9		prid2g 4725	. . . . 5 ⊢ (𝐵 ∈ V → 𝐵 ∈ {𝐴, 𝐵})
10	9	adantr 480	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ {𝐴, 𝐵})
11	8, 10	eqeltrd 2828	. . 3 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → ∪ {𝐴, 𝐵} ∈ {𝐴, 𝐵})
12		biid 261	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) ↔ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵))
13	12	bianass 642	. . . 4 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) ↔ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵))
14		inteq 4913	. . . . . . . . . 10 ⊢ (𝑥 = {𝐴} → ∩ 𝑥 = ∩ {𝐴})
15		intsng 4947	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴)
16	15	adantl 481	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐴} = 𝐴)
17	14, 16	sylan9eqr 2786	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 = 𝐴)
18		prid1g 4724	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
19	18	adantl 481	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ {𝐴, 𝐵})
20	19	adantr 480	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → 𝐴 ∈ {𝐴, 𝐵})
21	17, 20	eqeltrd 2828	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐴}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
22	21	ex 412	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
23	22	adantr 480	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
24		inteq 4913	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐵} → ∩ 𝑥 = ∩ {𝐵})
25		intsng 4947	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ V → ∩ {𝐵} = 𝐵)
26	25	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → ∩ {𝐵} = 𝐵)
27	24, 26	sylan9eqr 2786	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 = 𝐵)
28	9	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → 𝐵 ∈ {𝐴, 𝐵})
29	27, 28	eqeltrd 2828	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 = {𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
30	29	ex 412	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
31	30	adantr 480	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
32		inteq 4913	. . . . . . . . . . 11 ⊢ (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 = ∩ {𝐴, 𝐵})
33	32	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = ∩ {𝐴, 𝐵})
34	1	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V))
35		intprg 4945	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ {𝐴, 𝐵} = (𝐴 ∩ 𝐵))
37		dfss2 3932	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
38	37	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐵) = 𝐴)
39	38	adantl 481	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∩ 𝐵) = 𝐴)
40	39	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → (𝐴 ∩ 𝐵) = 𝐴)
41	33, 36, 40	3eqtrd 2768	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 = 𝐴)
42	18	ad3antlr 731	. . . . . . . . 9 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → 𝐴 ∈ {𝐴, 𝐵})
43	41, 42	eqeltrd 2828	. . . . . . . 8 ⊢ ((((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵})
44	43	ex 412	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → (𝑥 = {𝐴, 𝐵} → ∩ 𝑥 ∈ {𝐴, 𝐵}))
45	31, 44	jaod 859	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
46	23, 45	jaod 859	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ⊆ 𝐵) → ((𝑥 = {𝐴} ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) → ∩ 𝑥 ∈ {𝐴, 𝐵}))
47		sspr 4799	. . . . . 6 ⊢ (𝑥 ⊆ {𝐴, 𝐵} ↔ ((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})))
48		andir 1010	. . . . . . 7 ⊢ ((((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∨ (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵})) ∧ 𝑥 ≠ ∅) ↔ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ∨ ((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅)))
49		andir 1010	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)))
50		eqneqall 2936	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑥 ≠ ∅ → ⊥))
51	50	imp 406	. . . . . . . . . . 11 ⊢ ((𝑥 = ∅ ∧ 𝑥 ≠ ∅) → ⊥)
52		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 = {𝐴} ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
53	51, 52	orim12i 908	. . . . . . . . . 10 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → (⊥ ∨ 𝑥 = {𝐴}))
54		falim 1557	. . . . . . . . . . 11 ⊢ (⊥ → 𝑥 = {𝐴})
55	54	bj-jaoi1 36559	. . . . . . . . . 10 ⊢ ((⊥ ∨ 𝑥 = {𝐴}) → 𝑥 = {𝐴})
56	53, 55	syl 17	. . . . . . . . 9 ⊢ (((𝑥 = ∅ ∧ 𝑥 ≠ ∅) ∨ (𝑥 = {𝐴} ∧ 𝑥 ≠ ∅)) → 𝑥 = {𝐴})
57	49, 56	sylbi 217	. . . . . . . 8 ⊢ (((𝑥 = ∅ ∨ 𝑥 = {𝐴}) ∧ 𝑥 ≠ ∅) → 𝑥 = {𝐴})
58		simpl 482	. . . . . . . 8 ⊢ (((𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}) ∧ 𝑥 ≠ ∅) → (𝑥 = {𝐵} ∨ 𝑥 = {𝐴, 𝐵}))
59	57, 58	orim12i 908	. . . . . . 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 37098	. 2 ⊢ ((𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
65		pm3.22 459	. . . . 5 ⊢ ((¬ 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
66	65	adantrr 717	. . . 4 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → (𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V))
67		prprc2 4730	. . . . . 6 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
68	67	adantl 481	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴, 𝐵} = {𝐴})
69	68	eqcomd 2735	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ V) → {𝐴} = {𝐴, 𝐵})
70	66, 69	syl 17	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} = {𝐴, 𝐵})
71		bj-snmoore 37101	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore)
72	71	ad2antrl 728	. . 3 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴} ∈ Moore)
73	70, 72	eqeltrrd 2829	. 2 ⊢ ((¬ 𝐵 ∈ V ∧ (𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵)) → {𝐴, 𝐵} ∈ Moore)
74	64, 73	pm2.61ian 811	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → {𝐴, 𝐵} ∈ Moore)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540  ⊥wfal 1552   ∈ wcel 2109   ≠ wne 2925  Vcvv 3447   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  {csn 4589  {cpr 4591  ∪ cuni 4871  ∩ cint 4910  Moorecmoore 37091

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-pw 4565  df-sn 4590  df-pr 4592  df-uni 4872  df-int 4911  df-bj-moore 37092

This theorem is referenced by: (None)