Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  onfrALTlem5 Structured version   Visualization version   GIF version

Theorem onfrALTlem5 39074
Description: Lemma for onfrALT 39081. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTlem5 ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
Distinct variable groups:   𝑎,𝑏,𝑦   𝑥,𝑏,𝑦

Proof of Theorem onfrALTlem5
StepHypRef Expression
1 vex 3234 . . . 4 𝑎 ∈ V
21inex1 4832 . . 3 (𝑎𝑥) ∈ V
3 sbcimg 3510 . . 3 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅)))
42, 3ax-mp 5 . 2 ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅))
5 sbcan 3511 . . . 4 ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) ↔ ([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥) ∧ [(𝑎𝑥) / 𝑏]𝑏 ≠ ∅))
6 sseq1 3659 . . . . . 6 (𝑏 = (𝑎𝑥) → (𝑏 ⊆ (𝑎𝑥) ↔ (𝑎𝑥) ⊆ (𝑎𝑥)))
72, 6sbcie 3503 . . . . 5 ([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥) ↔ (𝑎𝑥) ⊆ (𝑎𝑥))
8 df-ne 2824 . . . . . . 7 (𝑏 ≠ ∅ ↔ ¬ 𝑏 = ∅)
98sbcbii 3524 . . . . . 6 ([(𝑎𝑥) / 𝑏]𝑏 ≠ ∅ ↔ [(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅)
10 sbcng 3509 . . . . . . . 8 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅ ↔ ¬ [(𝑎𝑥) / 𝑏]𝑏 = ∅))
1110bicomd 213 . . . . . . 7 ((𝑎𝑥) ∈ V → (¬ [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅))
122, 11ax-mp 5 . . . . . 6 [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ [(𝑎𝑥) / 𝑏] ¬ 𝑏 = ∅)
13 eqsbc3 3508 . . . . . . . 8 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎𝑥) = ∅))
142, 13ax-mp 5 . . . . . . 7 ([(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎𝑥) = ∅)
1514necon3bbii 2870 . . . . . 6 [(𝑎𝑥) / 𝑏]𝑏 = ∅ ↔ (𝑎𝑥) ≠ ∅)
169, 12, 153bitr2i 288 . . . . 5 ([(𝑎𝑥) / 𝑏]𝑏 ≠ ∅ ↔ (𝑎𝑥) ≠ ∅)
177, 16anbi12i 733 . . . 4 (([(𝑎𝑥) / 𝑏]𝑏 ⊆ (𝑎𝑥) ∧ [(𝑎𝑥) / 𝑏]𝑏 ≠ ∅) ↔ ((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅))
185, 17bitri 264 . . 3 ([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) ↔ ((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅))
19 df-rex 2947 . . . . 5 (∃𝑦𝑏 (𝑏𝑦) = ∅ ↔ ∃𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅))
2019sbcbii 3524 . . . 4 ([(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅ ↔ [(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅))
21 sbcan 3511 . . . . . . 7 ([(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ([(𝑎𝑥) / 𝑏]𝑦𝑏[(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅))
22 sbcel2gv 3529 . . . . . . . . 9 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏]𝑦𝑏𝑦 ∈ (𝑎𝑥)))
232, 22ax-mp 5 . . . . . . . 8 ([(𝑎𝑥) / 𝑏]𝑦𝑏𝑦 ∈ (𝑎𝑥))
24 sbceqg 4017 . . . . . . . . . 10 ((𝑎𝑥) ∈ V → ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ (𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏∅))
252, 24ax-mp 5 . . . . . . . . 9 ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ (𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏∅)
26 csbin 4043 . . . . . . . . . . 11 (𝑎𝑥) / 𝑏(𝑏𝑦) = ((𝑎𝑥) / 𝑏𝑏(𝑎𝑥) / 𝑏𝑦)
27 csbvarg 4036 . . . . . . . . . . . . 13 ((𝑎𝑥) ∈ V → (𝑎𝑥) / 𝑏𝑏 = (𝑎𝑥))
282, 27ax-mp 5 . . . . . . . . . . . 12 (𝑎𝑥) / 𝑏𝑏 = (𝑎𝑥)
29 csbconstg 3579 . . . . . . . . . . . . 13 ((𝑎𝑥) ∈ V → (𝑎𝑥) / 𝑏𝑦 = 𝑦)
302, 29ax-mp 5 . . . . . . . . . . . 12 (𝑎𝑥) / 𝑏𝑦 = 𝑦
3128, 30ineq12i 3845 . . . . . . . . . . 11 ((𝑎𝑥) / 𝑏𝑏(𝑎𝑥) / 𝑏𝑦) = ((𝑎𝑥) ∩ 𝑦)
3226, 31eqtri 2673 . . . . . . . . . 10 (𝑎𝑥) / 𝑏(𝑏𝑦) = ((𝑎𝑥) ∩ 𝑦)
33 csb0 4015 . . . . . . . . . 10 (𝑎𝑥) / 𝑏∅ = ∅
3432, 33eqeq12i 2665 . . . . . . . . 9 ((𝑎𝑥) / 𝑏(𝑏𝑦) = (𝑎𝑥) / 𝑏∅ ↔ ((𝑎𝑥) ∩ 𝑦) = ∅)
3525, 34bitri 264 . . . . . . . 8 ([(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅ ↔ ((𝑎𝑥) ∩ 𝑦) = ∅)
3623, 35anbi12i 733 . . . . . . 7 (([(𝑎𝑥) / 𝑏]𝑦𝑏[(𝑎𝑥) / 𝑏](𝑏𝑦) = ∅) ↔ (𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
3721, 36bitri 264 . . . . . 6 ([(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ (𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
3837exbii 1814 . . . . 5 (∃𝑦[(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦(𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
39 sbcex2 3519 . . . . 5 ([(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦[(𝑎𝑥) / 𝑏](𝑦𝑏 ∧ (𝑏𝑦) = ∅))
40 df-rex 2947 . . . . 5 (∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅ ↔ ∃𝑦(𝑦 ∈ (𝑎𝑥) ∧ ((𝑎𝑥) ∩ 𝑦) = ∅))
4138, 39, 403bitr4i 292 . . . 4 ([(𝑎𝑥) / 𝑏]𝑦(𝑦𝑏 ∧ (𝑏𝑦) = ∅) ↔ ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅)
4220, 41bitri 264 . . 3 ([(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅ ↔ ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅)
4318, 42imbi12i 339 . 2 (([(𝑎𝑥) / 𝑏](𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → [(𝑎𝑥) / 𝑏]𝑦𝑏 (𝑏𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
444, 43bitri 264 1 ([(𝑎𝑥) / 𝑏]((𝑏 ⊆ (𝑎𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦𝑏 (𝑏𝑦) = ∅) ↔ (((𝑎𝑥) ⊆ (𝑎𝑥) ∧ (𝑎𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎𝑥)((𝑎𝑥) ∩ 𝑦) = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  wne 2823  wrex 2942  Vcvv 3231  [wsbc 3468  csb 3566  cin 3606  wss 3607  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949
This theorem is referenced by:  onfrALTlem3  39076  onfrALTlem3VD  39437
  Copyright terms: Public domain W3C validator