Metamath Proof Explorer


Theorem en3lplem1

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

Ref Expression
Assertion en3lplem1
|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> ( x i^i { A , B , C } ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 simp3
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> C e. A )
2 eleq2
 |-  ( x = A -> ( C e. x <-> C e. A ) )
3 1 2 syl5ibrcom
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> C e. x ) )
4 tpid3g
 |-  ( C e. A -> C e. { A , B , C } )
5 4 3ad2ant3
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> C e. { A , B , C } )
6 inelcm
 |-  ( ( C e. x /\ C e. { A , B , C } ) -> ( x i^i { A , B , C } ) =/= (/) )
7 5 6 sylan2
 |-  ( ( C e. x /\ ( A e. B /\ B e. C /\ C e. A ) ) -> ( x i^i { A , B , C } ) =/= (/) )
8 7 expcom
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( C e. x -> ( x i^i { A , B , C } ) =/= (/) ) )
9 3 8 syld
 |-  ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> ( x i^i { A , B , C } ) =/= (/) ) )