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

Theorem onfrALTVD 43155
Description: Virtual deduction proof of onfrALT 42813. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALT 42813 is onfrALTVD 43155 without virtual deductions and was automatically derived from onfrALTVD 43155.
1:: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥𝑎 ∧ ¬ (𝑎𝑥) = ∅)   ▶   𝑦𝑎(𝑎𝑦) = ∅   )
2:: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥𝑎 ∧ (𝑎𝑥) = ∅)   ▶   𝑦𝑎(𝑎𝑦) = ∅   )
3:1: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥𝑎   ▶    (¬ (𝑎𝑥) = ∅ → ∃𝑦𝑎(𝑎𝑦) = ∅)   )
4:2: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥𝑎   ▶    ((𝑎𝑥) = ∅ → ∃𝑦𝑎(𝑎𝑦) = ∅)   )
5:: ((𝑎𝑥) = ∅ ∨ ¬ (𝑎𝑥) = ∅)
6:5,4,3: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥𝑎   ▶    𝑦𝑎(𝑎𝑦) = ∅   )
7:6: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑥𝑎 → ∃𝑦𝑎(𝑎𝑦) = ∅)   )
8:7: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑥(𝑥 𝑎 → ∃𝑦𝑎(𝑎𝑦) = ∅)   )
9:8: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (∃𝑥𝑥 𝑎 → ∃𝑦𝑎(𝑎𝑦) = ∅)   )
10:: (𝑎 ≠ ∅ ↔ ∃𝑥𝑥𝑎)
11:9,10: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ∅ → ∃𝑦𝑎(𝑎𝑦) = ∅)   )
12:: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 On ∧ 𝑎 ≠ ∅)   )
13:12: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎    )
14:13,11: (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑦 𝑎(𝑎𝑦) = ∅   )
15:14: ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅)
16:15: 𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦 𝑎(𝑎𝑦) = ∅)
qed:16: E Fr On
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTVD E Fr On

Proof of Theorem onfrALTVD
Dummy variables 𝑥 𝑎 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 42838 . . . . . 6 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
2 simpr 485 . . . . . 6 ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
31, 2e1a 42891 . . . . 5 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ≠ ∅   )
4 exmid 893 . . . . . . . . . 10 ((𝑎𝑥) = ∅ ∨ ¬ (𝑎𝑥) = ∅)
5 onfrALTlem1VD 43154 . . . . . . . . . . 11 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥𝑎 ∧ (𝑎𝑥) = ∅)   ▶   𝑦𝑎 (𝑎𝑦) = ∅   )
65in2an 42872 . . . . . . . . . 10 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥𝑎   ▶   ((𝑎𝑥) = ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅)   )
7 onfrALTlem2VD 43153 . . . . . . . . . . 11 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥𝑎 ∧ ¬ (𝑎𝑥) = ∅)   ▶   𝑦𝑎 (𝑎𝑦) = ∅   )
87in2an 42872 . . . . . . . . . 10 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥𝑎   ▶   (¬ (𝑎𝑥) = ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅)   )
9 pm2.61 191 . . . . . . . . . . 11 (((𝑎𝑥) = ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅) → ((¬ (𝑎𝑥) = ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅))
109a1i 11 . . . . . . . . . 10 (((𝑎𝑥) = ∅ ∨ ¬ (𝑎𝑥) = ∅) → (((𝑎𝑥) = ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅) → ((¬ (𝑎𝑥) = ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅)))
114, 6, 8, 10e022 42905 . . . . . . . . 9 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥𝑎   ▶   𝑦𝑎 (𝑎𝑦) = ∅   )
1211in2 42869 . . . . . . . 8 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅)   )
1312gen11 42880 . . . . . . 7 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑥(𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅)   )
14 19.23v 1945 . . . . . . . 8 (∀𝑥(𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅) ↔ (∃𝑥 𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅))
1514biimpi 215 . . . . . . 7 (∀𝑥(𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅) → (∃𝑥 𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅))
1613, 15e1a 42891 . . . . . 6 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (∃𝑥 𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅)   )
17 n0 4306 . . . . . 6 (𝑎 ≠ ∅ ↔ ∃𝑥 𝑥𝑎)
18 imbi1 347 . . . . . . 7 ((𝑎 ≠ ∅ ↔ ∃𝑥 𝑥𝑎) → ((𝑎 ≠ ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅) ↔ (∃𝑥 𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅)))
1918biimprcd 249 . . . . . 6 ((∃𝑥 𝑥𝑎 → ∃𝑦𝑎 (𝑎𝑦) = ∅) → ((𝑎 ≠ ∅ ↔ ∃𝑥 𝑥𝑎) → (𝑎 ≠ ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅)))
2016, 17, 19e10 42958 . . . . 5 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ≠ ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅)   )
21 pm2.27 42 . . . . 5 (𝑎 ≠ ∅ → ((𝑎 ≠ ∅ → ∃𝑦𝑎 (𝑎𝑦) = ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅))
223, 20, 21e11 42952 . . . 4 (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑦𝑎 (𝑎𝑦) = ∅   )
2322in1 42835 . . 3 ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅)
2423ax-gen 1797 . 2 𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅)
25 dfepfr 5618 . . 3 ( E Fr On ↔ ∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅))
2625biimpri 227 . 2 (∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦𝑎 (𝑎𝑦) = ∅) → E Fr On)
2724, 26e0a 43036 1 E Fr On
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  wal 1539   = wceq 1541  wex 1781  wcel 2106  wne 2943  wrex 3073  cin 3909  wss 3910  c0 4282   E cep 5536   Fr wfr 5585  Oncon0 6317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2370  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-tr 5223  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-ord 6320  df-on 6321  df-vd1 42834  df-vd2 42842  df-vd3 42854
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator