Theorem en3lplem1

Description: Lemma for en3lp . (Contributed by Alan Sare, 28-Oct-2011)

	Ref	Expression
Assertion	en3lplem1	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐴 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ 𝐴 )
2		eleq2	⊢ ( 𝑥 = 𝐴 → ( 𝐶 ∈ 𝑥 ↔ 𝐶 ∈ 𝐴 ) )
3	1 2	syl5ibrcom	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐴 → 𝐶 ∈ 𝑥 ) )
4		tpid3g	⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
6		inelcm	⊢ ( ( 𝐶 ∈ 𝑥 ∧ 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ )
7	5 6	sylan2	⊢ ( ( 𝐶 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ )
8	7	expcom	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ∈ 𝑥 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )
9	3 8	syld	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑥 = 𝐴 → ( 𝑥 ∩ { 𝐴 , 𝐵 , 𝐶 } ) ≠ ∅ ) )