Metamath Proof Explorer

Theorem en3lplem1

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

Ref Expression
Assertion en3lplem1 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → x ∩ A B C ≠ ∅

Proof

Step Hyp Ref Expression
1 simp3 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → C ∈ A
2 eleq2 ⊢ x = A → C ∈ x ↔ C ∈ A
3 1 2 syl5ibrcom ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → C ∈ x
4 tpid3g ⊢ C ∈ A → C ∈ A B C
5 4 3ad2ant3 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → C ∈ A B C
6 inelcm ⊢ C ∈ x ∧ C ∈ A B C → x ∩ A B C ≠ ∅
7 5 6 sylan2 ⊢ C ∈ x ∧ A ∈ B ∧ B ∈ C ∧ C ∈ A → x ∩ A B C ≠ ∅
8 7 expcom ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → C ∈ x → x ∩ A B C ≠ ∅
9 3 8 syld ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → x ∩ A B C ≠ ∅