Metamath Proof Explorer

Theorem en3lpVD

Description: Virtual deduction proof of en3lp . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en3lpVD ⊢¬A∈B∧B∈C∧C∈A

Proof

Step Hyp Ref Expression
1 pm2.1 ⊢¬ABC=∅∨ABC=∅
2 df-ne ⊢ABC≠∅↔¬ABC=∅
3 2 bicomi ⊢¬ABC=∅↔ABC≠∅
4 3 orbi1i ⊢¬ABC=∅∨ABC=∅↔ABC≠∅∨ABC=∅
5 1 4 mpbi ⊢ABC≠∅∨ABC=∅
6 zfregs2 ⊢ABC≠∅→¬∀x∈ABC∃yy∈ABC∧y∈x
7 en3lplem2VD ⊢A∈B∧B∈C∧C∈A→x∈ABC→∃yy∈ABC∧y∈x
8 7 alrimiv ⊢A∈B∧B∈C∧C∈A→∀xx∈ABC→∃yy∈ABC∧y∈x
9 df-ral ⊢∀x∈ABC∃yy∈ABC∧y∈x↔∀xx∈ABC→∃yy∈ABC∧y∈x
10 8 9 sylibr ⊢A∈B∧B∈C∧C∈A→∀x∈ABC∃yy∈ABC∧y∈x
11 10 con3i ⊢¬∀x∈ABC∃yy∈ABC∧y∈x→¬A∈B∧B∈C∧C∈A
12 6 11 syl ⊢ABC≠∅→¬A∈B∧B∈C∧C∈A
13 idn1 ⊢ABC=∅→ABC=∅
14 noel ⊢¬C∈∅
15 eleq2 ⊢ABC=∅→C∈ABC↔C∈∅
16 15 notbid ⊢ABC=∅→¬C∈ABC↔¬C∈∅
17 16 biimprd ⊢ABC=∅→¬C∈∅→¬C∈ABC
18 13 14 17 e10 ⊢ABC=∅→¬C∈ABC
19 tpid3g ⊢C∈A→C∈ABC
20 19 con3i ⊢¬C∈ABC→¬C∈A
21 18 20 e1a ⊢ABC=∅→¬C∈A
22 simp3 ⊢A∈B∧B∈C∧C∈A→C∈A
23 22 con3i ⊢¬C∈A→¬A∈B∧B∈C∧C∈A
24 21 23 e1a ⊢ABC=∅→¬A∈B∧B∈C∧C∈A
25 24 in1 ⊢ABC=∅→¬A∈B∧B∈C∧C∈A
26 12 25 jaoi ⊢ABC≠∅∨ABC=∅→¬A∈B∧B∈C∧C∈A
27 5 26 ax-mp ⊢¬A∈B∧B∈C∧C∈A