Theorem onfrALTVD 45347

Description: Virtual deduction proof of onfrALT 45006. 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 45006 is onfrALTVD 45347 without virtual deductions and was automatically derived from onfrALTVD 45347.

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.

Step	Hyp	Ref	Expression
1		idn1 45031	. . . . . 6 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   )
2		simpr 486	. . . . . 6 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → 𝑎 ≠ ∅)
3	1, 2	e1a 45084	. . . . 5 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   𝑎 ≠ ∅   )
4		exmid 901	. . . . . . . . . 10 ⊢ ((𝑎 ∩ 𝑥) = ∅ ∨ ¬ (𝑎 ∩ 𝑥) = ∅)
5		onfrALTlem1VD 45346	. . . . . . . . . . 11 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )
6	5	in2an 45065	. . . . . . . . . 10 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶   ((𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   )
7		onfrALTlem2VD 45345	. . . . . . . . . . 11 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   (𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )
8	7	in2an 45065	. . . . . . . . . 10 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶   (¬ (𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   )
9		pm2.61 193	. . . . . . . . . . 11 ⊢ (((𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ((¬ (𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))
10	9	a1i 11	. . . . . . . . . 10 ⊢ (((𝑎 ∩ 𝑥) = ∅ ∨ ¬ (𝑎 ∩ 𝑥) = ∅) → (((𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ((¬ (𝑎 ∩ 𝑥) = ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)))
11	4, 6, 8, 10	e022 45098	. . . . . . . . 9 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ,   𝑥 ∈ 𝑎   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )
12	11	in2 45062	. . . . . . . 8 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   )
13	12	gen11 45073	. . . . . . 7 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   ∀𝑥(𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   )
14		19.23v 1950	. . . . . . . 8 ⊢ (∀𝑥(𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) ↔ (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))
15	14	biimpi 218	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))
16	13, 15	e1a 45084	. . . . . 6 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   )
17		n0 4283	. . . . . 6 ⊢ (𝑎 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑎)
18		imbi1 349	. . . . . . 7 ⊢ ((𝑎 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑎) → ((𝑎 ≠ ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) ↔ (∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)))
19	18	biimprcd 252	. . . . . 6 ⊢ ((∃𝑥 𝑥 ∈ 𝑎 → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ((𝑎 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝑎) → (𝑎 ≠ ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)))
20	16, 17, 19	e10 45151	. . . . 5 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   (𝑎 ≠ ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)   )
21		pm2.27 42	. . . . 5 ⊢ (𝑎 ≠ ∅ → ((𝑎 ≠ ∅ → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))
22	3, 20, 21	e11 45145	. . . 4 ⊢ (   (𝑎 ⊆ On ∧ 𝑎 ≠ ∅)   ▶   ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅   )
23	22	in1 45028	. . 3 ⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)
24	23	ax-gen 1803	. 2 ⊢ ∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅)
25		dfepfr 5604	. . 3 ⊢ ( E Fr On ↔ ∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))
26	25	biimpri 230	. 2 ⊢ (∀𝑎((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅) → E Fr On)
27	24, 26	e0a 45228	1 ⊢ E Fr On

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 397   ∨ wo 854  ∀wal 1546   = wceq 1548  ∃wex 1787   ∈ wcel 2121   ≠ wne 2936  ∃wrex 3065   ∩ cin 3883   ⊆ wss 3884  ∅c0 4263   E cep 5519   Fr wfr 5570  Oncon0 6313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-13 2382  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3725  df-csb 3833  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-tr 5182  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-ord 6316  df-on 6317  df-vd1 45027  df-vd2 45035  df-vd3 45047

This theorem is referenced by: (None)