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