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 ⊢ ¬ A B C = ∅ ∨ A B C = ∅
2 df-ne ⊢ A B C ≠ ∅ ↔ ¬ A B C = ∅
3 2 bicomi ⊢ ¬ A B C = ∅ ↔ A B C ≠ ∅
4 3 orbi1i ⊢ ¬ A B C = ∅ ∨ A B C = ∅ ↔ A B C ≠ ∅ ∨ A B C = ∅
5 1 4 mpbi ⊢ A B C ≠ ∅ ∨ A B C = ∅
6 zfregs2 ⊢ A B C ≠ ∅ → ¬ ∀ x ∈ A B C ∃ y y ∈ A B C ∧ y ∈ x
7 en3lplem2VD ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∈ A B C → ∃ y y ∈ A B C ∧ y ∈ x
8 7 alrimiv ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → ∀ x x ∈ A B C → ∃ y y ∈ A B C ∧ y ∈ x
9 df-ral ⊢ ∀ x ∈ A B C ∃ y y ∈ A B C ∧ y ∈ x ↔ ∀ x x ∈ A B C → ∃ y y ∈ A B C ∧ y ∈ x
10 8 9 sylibr ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → ∀ x ∈ A B C ∃ y y ∈ A B C ∧ y ∈ x
11 10 con3i ⊢ ¬ ∀ x ∈ A B C ∃ y y ∈ A B C ∧ y ∈ x → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
12 6 11 syl ⊢ A B C ≠ ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
13 idn1 ⊢ A B C = ∅ → A B C = ∅
14 noel ⊢ ¬ C ∈ ∅
15 eleq2 ⊢ A B C = ∅ → C ∈ A B C ↔ C ∈ ∅
16 15 notbid ⊢ A B C = ∅ → ¬ C ∈ A B C ↔ ¬ C ∈ ∅
17 16 biimprd ⊢ A B C = ∅ → ¬ C ∈ ∅ → ¬ C ∈ A B C
18 13 14 17 e10 ⊢ A B C = ∅ → ¬ C ∈ A B C
19 tpid3g ⊢ C ∈ A → C ∈ A B C
20 19 con3i ⊢ ¬ C ∈ A B C → ¬ C ∈ A
21 18 20 e1a ⊢ A B C = ∅ → ¬ 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 ⊢ A B C = ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
25 24 in1 ⊢ A B C = ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
26 12 25 jaoi ⊢ A B C ≠ ∅ ∨ A B C = ∅ → ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A
27 5 26 ax-mp ⊢ ¬ A ∈ B ∧ B ∈ C ∧ C ∈ A