Theorem bj-ismooredr2 33065

Description: Sufficient condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021.)

Hypotheses

Ref	Expression
bj-ismooredr2.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
bj-ismooredr2.2	⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴)
bj-ismooredr2.3	⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)

Assertion

Ref	Expression
bj-ismooredr2	⊢ (𝜑 → 𝐴 ∈ Moore)

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem bj-ismooredr2

Step	Hyp	Ref	Expression
1		selpw 4165	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
2		pm2.1 433	. . . . . . . 8 ⊢ (¬ 𝑥 = ∅ ∨ 𝑥 = ∅)
3	2	biantru 526	. . . . . . 7 ⊢ (𝑥 ⊆ 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ (¬ 𝑥 = ∅ ∨ 𝑥 = ∅)))
4		andi 911	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ (¬ 𝑥 = ∅ ∨ 𝑥 = ∅)) ↔ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 = ∅) ∨ (𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅)))
5	3, 4	bitri 264	. . . . . 6 ⊢ (𝑥 ⊆ 𝐴 ↔ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 = ∅) ∨ (𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅)))
6		df-ne 2795	. . . . . . . . 9 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
7	6	bicomi 214	. . . . . . . 8 ⊢ (¬ 𝑥 = ∅ ↔ 𝑥 ≠ ∅)
8	7	anbi2i 730	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 = ∅) ↔ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅))
9		simpr 477	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅) → 𝑥 = ∅)
10		id 22	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → 𝑥 = ∅)
11		0ss 3972	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐴
12	10, 11	syl6eqss 3655	. . . . . . . . 9 ⊢ (𝑥 = ∅ → 𝑥 ⊆ 𝐴)
13	12	ancri 575	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅))
14	9, 13	impbii 199	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅) ↔ 𝑥 = ∅)
15	8, 14	orbi12i 543	. . . . . 6 ⊢ (((𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 = ∅) ∨ (𝑥 ⊆ 𝐴 ∧ 𝑥 = ∅)) ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∨ 𝑥 = ∅))
16	5, 15	bitri 264	. . . . 5 ⊢ (𝑥 ⊆ 𝐴 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∨ 𝑥 = ∅))
17	1, 16	bitri 264	. . . 4 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∨ 𝑥 = ∅))
18		bj-ismooredr2.3	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)
19	18	expl 648	. . . . . 6 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴))
20		intssuni2 4502	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ⊆ ∪ 𝐴)
21		sseqin2 3817	. . . . . . . . . . 11 ⊢ (∩ 𝑥 ⊆ ∪ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑥) = ∩ 𝑥)
22	21	biimpi 206	. . . . . . . . . 10 ⊢ (∩ 𝑥 ⊆ ∪ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) = ∩ 𝑥)
23	22	eqcomd 2628	. . . . . . . . 9 ⊢ (∩ 𝑥 ⊆ ∪ 𝐴 → ∩ 𝑥 = (∪ 𝐴 ∩ ∩ 𝑥))
24	23	eleq1d 2686	. . . . . . . 8 ⊢ (∩ 𝑥 ⊆ ∪ 𝐴 → (∩ 𝑥 ∈ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
25	24	biimpd 219	. . . . . . 7 ⊢ (∩ 𝑥 ⊆ ∪ 𝐴 → (∩ 𝑥 ∈ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
26	20, 25	syl 17	. . . . . 6 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∩ 𝑥 ∈ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
27	19, 26	sylcom 30	. . . . 5 ⊢ (𝜑 → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
28		bj-ismooredr2.2	. . . . . 6 ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴)
29		rint0 4517	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∪ 𝐴 ∩ ∩ 𝑥) = ∪ 𝐴)
30	29	eqcomd 2628	. . . . . . 7 ⊢ (𝑥 = ∅ → ∪ 𝐴 = (∪ 𝐴 ∩ ∩ 𝑥))
31	30	eleq1d 2686	. . . . . 6 ⊢ (𝑥 = ∅ → (∪ 𝐴 ∈ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
32	28, 31	syl5ibcom 235	. . . . 5 ⊢ (𝜑 → (𝑥 = ∅ → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
33	27, 32	jaod 395	. . . 4 ⊢ (𝜑 → (((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) ∨ 𝑥 = ∅) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
34	17, 33	syl5bi 232	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
35	34	ralrimiv 2965	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)
36		bj-ismooredr2.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
37		bj-ismoore 33059	. . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
38	36, 37	syl 17	. 2 ⊢ (𝜑 → (𝐴 ∈ Moore ↔ ∀𝑥 ∈ 𝒫 𝐴(∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
39	35, 38	mpbird 247	1 ⊢ (𝜑 → 𝐴 ∈ Moore)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158  ∪ cuni 4436  ∩ cint 4475  Moorecmoore 33057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-uni 4437  df-int 4476  df-bj-moore 33058

This theorem is referenced by:  bj-snmoore  33068