This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 pm2.1 ⊢ ( ¬ { 𝐴 , 𝐵 , 𝐶 } = ∅ ∨ { 𝐴 , 𝐵 , 𝐶 } = ∅ )
2 df-ne ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ ↔ ¬ { 𝐴 , 𝐵 , 𝐶 } = ∅ )
3 2 bicomi ⊢ ( ¬ { 𝐴 , 𝐵 , 𝐶 } = ∅ ↔ { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )
4 3 orbi1i ⊢ ( ( ¬ { 𝐴 , 𝐵 , 𝐶 } = ∅ ∨ { 𝐴 , 𝐵 , 𝐶 } = ∅ ) ↔ ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ ∨ { 𝐴 , 𝐵 , 𝐶 } = ∅ ) )
5 1 4 mpbi ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ ∨ { 𝐴 , 𝐵 , 𝐶 } = ∅ )
6 zfregs2 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ → ¬ ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )
7 en3lplem2VD ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )
8 7 alrimiv ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ∀ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )
9 df-ral ⊢ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) ) )
10 8 9 sylibr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) )
11 10 con3i ⊢ ( ¬ ∀ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ∃ 𝑦 ( 𝑦 ∈ { 𝐴 , 𝐵 , 𝐶 } ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
12 6 11 syl ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
13 idn1 ⊢ (    { 𝐴 , 𝐵 , 𝐶 } = ∅    ▶    { 𝐴 , 𝐵 , 𝐶 } = ∅    )
14 noel ⊢ ¬ 𝐶 ∈ ∅
15 eleq2 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ( 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐶 ∈ ∅ ) )
16 15 notbid ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ( ¬ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ¬ 𝐶 ∈ ∅ ) )
17 16 biimprd ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ( ¬ 𝐶 ∈ ∅ → ¬ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ) )
18 13 14 17 e10 ⊢ (    { 𝐴 , 𝐵 , 𝐶 } = ∅    ▶    ¬ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 }    )
19 tpid3g ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
20 19 con3i ⊢ ( ¬ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } → ¬ 𝐶 ∈ 𝐴 )
21 18 20 e1a ⊢ (    { 𝐴 , 𝐵 , 𝐶 } = ∅    ▶    ¬ 𝐶 ∈ 𝐴    )
22 simp3 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ 𝐴 )
23 22 con3i ⊢ ( ¬ 𝐶 ∈ 𝐴 → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
24 21 23 e1a ⊢ (    { 𝐴 , 𝐵 , 𝐶 } = ∅    ▶    ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )    )
25 24 in1 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
26 12 25 jaoi ⊢ ( ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ ∨ { 𝐴 , 𝐵 , 𝐶 } = ∅ ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
27 5 26 ax-mp ⊢ ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )