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

Metamath Proof Explorer

Theorem en3lp

Description: No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD using a translation program. (Contributed by Alan Sare, 24-Oct-2011)

Ref Expression
Assertion en3lp ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ 𝐶 ∈ ∅
2 eleq2 ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ( 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐶 ∈ ∅ ) )
3 1 2 mtbiri ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ¬ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
4 tpid3g ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
5 3 4 nsyl ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ¬ 𝐶 ∈ 𝐴 )
6 5 intn3an3d ⊢ ( { 𝐴 , 𝐵 , 𝐶 } = ∅ → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
7 tpex ⊢ { 𝐴 , 𝐵 , 𝐶 } ∈ V
8 zfreg ⊢ ( ( { 𝐴 , 𝐵 , 𝐶 } ∈ V ∧ { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) = ∅ )
9 7 8 mpan ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ → ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) = ∅ )
10 en3lplem2 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )
11 10 com12 ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )
12 11 necon2bd ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) = ∅ → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ) )
13 12 rexlimiv ⊢ ( ∃ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) = ∅ → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
14 9 13 syl ⊢ ( { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) )
15 6 14 pm2.61ine ⊢ ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 )