Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-ismooredr2 Structured version   Visualization version   GIF version

Theorem bj-ismooredr2 33367
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
StepHypRef Expression
1 selpw 4305 . . . . 5 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
2 pm2.1 432 . . . . . . . 8 𝑥 = ∅ ∨ 𝑥 = ∅)
32biantru 527 . . . . . . 7 (𝑥𝐴 ↔ (𝑥𝐴 ∧ (¬ 𝑥 = ∅ ∨ 𝑥 = ∅)))
4 andi 947 . . . . . . 7 ((𝑥𝐴 ∧ (¬ 𝑥 = ∅ ∨ 𝑥 = ∅)) ↔ ((𝑥𝐴 ∧ ¬ 𝑥 = ∅) ∨ (𝑥𝐴𝑥 = ∅)))
53, 4bitri 264 . . . . . 6 (𝑥𝐴 ↔ ((𝑥𝐴 ∧ ¬ 𝑥 = ∅) ∨ (𝑥𝐴𝑥 = ∅)))
6 df-ne 2929 . . . . . . . . 9 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
76bicomi 214 . . . . . . . 8 𝑥 = ∅ ↔ 𝑥 ≠ ∅)
87anbi2i 732 . . . . . . 7 ((𝑥𝐴 ∧ ¬ 𝑥 = ∅) ↔ (𝑥𝐴𝑥 ≠ ∅))
9 simpr 479 . . . . . . . 8 ((𝑥𝐴𝑥 = ∅) → 𝑥 = ∅)
10 id 22 . . . . . . . . . 10 (𝑥 = ∅ → 𝑥 = ∅)
11 0ss 4111 . . . . . . . . . 10 ∅ ⊆ 𝐴
1210, 11syl6eqss 3792 . . . . . . . . 9 (𝑥 = ∅ → 𝑥𝐴)
1312ancri 576 . . . . . . . 8 (𝑥 = ∅ → (𝑥𝐴𝑥 = ∅))
149, 13impbii 199 . . . . . . 7 ((𝑥𝐴𝑥 = ∅) ↔ 𝑥 = ∅)
158, 14orbi12i 544 . . . . . 6 (((𝑥𝐴 ∧ ¬ 𝑥 = ∅) ∨ (𝑥𝐴𝑥 = ∅)) ↔ ((𝑥𝐴𝑥 ≠ ∅) ∨ 𝑥 = ∅))
165, 15bitri 264 . . . . 5 (𝑥𝐴 ↔ ((𝑥𝐴𝑥 ≠ ∅) ∨ 𝑥 = ∅))
171, 16bitri 264 . . . 4 (𝑥 ∈ 𝒫 𝐴 ↔ ((𝑥𝐴𝑥 ≠ ∅) ∨ 𝑥 = ∅))
18 bj-ismooredr2.3 . . . . . . 7 (((𝜑𝑥𝐴) ∧ 𝑥 ≠ ∅) → 𝑥𝐴)
1918expl 649 . . . . . 6 (𝜑 → ((𝑥𝐴𝑥 ≠ ∅) → 𝑥𝐴))
20 intssuni2 4650 . . . . . . 7 ((𝑥𝐴𝑥 ≠ ∅) → 𝑥 𝐴)
21 sseqin2 3956 . . . . . . . . . . 11 ( 𝑥 𝐴 ↔ ( 𝐴 𝑥) = 𝑥)
2221biimpi 206 . . . . . . . . . 10 ( 𝑥 𝐴 → ( 𝐴 𝑥) = 𝑥)
2322eqcomd 2762 . . . . . . . . 9 ( 𝑥 𝐴 𝑥 = ( 𝐴 𝑥))
2423eleq1d 2820 . . . . . . . 8 ( 𝑥 𝐴 → ( 𝑥𝐴 ↔ ( 𝐴 𝑥) ∈ 𝐴))
2524biimpd 219 . . . . . . 7 ( 𝑥 𝐴 → ( 𝑥𝐴 → ( 𝐴 𝑥) ∈ 𝐴))
2620, 25syl 17 . . . . . 6 ((𝑥𝐴𝑥 ≠ ∅) → ( 𝑥𝐴 → ( 𝐴 𝑥) ∈ 𝐴))
2719, 26sylcom 30 . . . . 5 (𝜑 → ((𝑥𝐴𝑥 ≠ ∅) → ( 𝐴 𝑥) ∈ 𝐴))
28 bj-ismooredr2.2 . . . . . 6 (𝜑 𝐴𝐴)
29 rint0 4665 . . . . . . . 8 (𝑥 = ∅ → ( 𝐴 𝑥) = 𝐴)
3029eqcomd 2762 . . . . . . 7 (𝑥 = ∅ → 𝐴 = ( 𝐴 𝑥))
3130eleq1d 2820 . . . . . 6 (𝑥 = ∅ → ( 𝐴𝐴 ↔ ( 𝐴 𝑥) ∈ 𝐴))
3228, 31syl5ibcom 235 . . . . 5 (𝜑 → (𝑥 = ∅ → ( 𝐴 𝑥) ∈ 𝐴))
3327, 32jaod 394 . . . 4 (𝜑 → (((𝑥𝐴𝑥 ≠ ∅) ∨ 𝑥 = ∅) → ( 𝐴 𝑥) ∈ 𝐴))
3417, 33syl5bi 232 . . 3 (𝜑 → (𝑥 ∈ 𝒫 𝐴 → ( 𝐴 𝑥) ∈ 𝐴))
3534ralrimiv 3099 . 2 (𝜑 → ∀𝑥 ∈ 𝒫 𝐴( 𝐴 𝑥) ∈ 𝐴)
36 bj-ismooredr2.1 . . 3 (𝜑𝐴𝑉)
37 bj-ismoore 33361 . . 3 (𝐴𝑉 → (𝐴Moore ↔ ∀𝑥 ∈ 𝒫 𝐴( 𝐴 𝑥) ∈ 𝐴))
3836, 37syl 17 . 2 (𝜑 → (𝐴Moore ↔ ∀𝑥 ∈ 𝒫 𝐴( 𝐴 𝑥) ∈ 𝐴))
3935, 38mpbird 247 1 (𝜑𝐴Moore)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1628  wcel 2135  wne 2928  wral 3046  cin 3710  wss 3711  c0 4054  𝒫 cpw 4298   cuni 4584   cint 4623  Moorecmoore 33359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-v 3338  df-dif 3714  df-in 3718  df-ss 3725  df-nul 4055  df-pw 4300  df-uni 4585  df-int 4624  df-bj-moore 33360
This theorem is referenced by:  bj-snmoore  33370
  Copyright terms: Public domain W3C validator