Theorem bj-ismooredr2 38222

Description: Sufficient condition to be a Moore collection (variant of bj-ismooredr 38221 singling out the empty intersection). There is no sethood hypothesis on 𝐴: it is a consequence of the first hypothesis. (Contributed by BJ, 9-Dec-2021.)

Hypotheses

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴

Proof of Theorem bj-ismooredr2

Step	Hyp	Ref	Expression
1		bj-ismooredr2.2	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)) → ∩ 𝑥 ∈ 𝐴)
2	1	anassrs 473	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ∈ 𝐴)
3		intssuni2 4936	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ⊆ ∪ 𝐴)
4		dfss 4098	. . . . . . . 8 ⊢ (∩ 𝑥 ⊆ ∪ 𝐴 ↔ ∩ 𝑥 = (∩ 𝑥 ∩ ∪ 𝐴))
5		incom 4109	. . . . . . . . . . 11 ⊢ (∩ 𝑥 ∩ ∪ 𝐴) = (∪ 𝐴 ∩ ∩ 𝑥)
6	5	eqeq2i 2776	. . . . . . . . . 10 ⊢ (∩ 𝑥 = (∩ 𝑥 ∩ ∪ 𝐴) ↔ ∩ 𝑥 = (∪ 𝐴 ∩ ∩ 𝑥))
7		eleq1 2852	. . . . . . . . . 10 ⊢ (∩ 𝑥 = (∪ 𝐴 ∩ ∩ 𝑥) → (∩ 𝑥 ∈ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
8	6, 7	sylbi 220	. . . . . . . . 9 ⊢ (∩ 𝑥 = (∩ 𝑥 ∩ ∪ 𝐴) → (∩ 𝑥 ∈ 𝐴 ↔ (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
9	8	biimpd 232	. . . . . . . 8 ⊢ (∩ 𝑥 = (∩ 𝑥 ∩ ∪ 𝐴) → (∩ 𝑥 ∈ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
10	4, 9	sylbi 220	. . . . . . 7 ⊢ (∩ 𝑥 ⊆ ∪ 𝐴 → (∩ 𝑥 ∈ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
11	3, 10	syl 18	. . . . . 6 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → (∩ 𝑥 ∈ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
12	11	adantll 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → (∩ 𝑥 ∈ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
13	2, 12	mpd 16	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)
14	13	ex 418	. . 3 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (𝑥 ≠ ∅ → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
15		nne 2963	. . . . 5 ⊢ (¬ 𝑥 ≠ ∅ ↔ 𝑥 = ∅)
16		bj-ismooredr2.1	. . . . . 6 ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴)
17		rint0 4951	. . . . . 6 ⊢ (𝑥 = ∅ → (∪ 𝐴 ∩ ∩ 𝑥) = ∪ 𝐴)
18		eleq1a 2859	. . . . . 6 ⊢ (∪ 𝐴 ∈ 𝐴 → ((∪ 𝐴 ∩ ∩ 𝑥) = ∪ 𝐴 → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
19	16, 17, 18	syl2im 41	. . . . 5 ⊢ (𝜑 → (𝑥 = ∅ → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
20	15, 19	biimtrid 245	. . . 4 ⊢ (𝜑 → (¬ 𝑥 ≠ ∅ → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
21	20	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (¬ 𝑥 ≠ ∅ → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴))
22	14, 21	pm2.61d 181	. 2 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝐴) → (∪ 𝐴 ∩ ∩ 𝑥) ∈ 𝐴)
23	22	bj-ismooredr 38221	1 ⊢ (𝜑 → 𝐴 ∈ Moore)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ≠ wne 2959   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281  ∪ cuni 4870  ∩ cint 4910  Moorecmoore 38215

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-nul 4282  df-pw 4562  df-uni 4871  df-int 4911  df-bj-moore 38216

This theorem is used by:  bj-snmoore  38225  bj-prmoore  38227