Theorem dford3lem1

Description: Lemma for dford3 . (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Assertion	dford3lem1	|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N ( Tr b /\ A. y e. b Tr y ) )

Proof

Step	Hyp	Ref	Expression
1		treq	|- ( y = b -> ( Tr y <-> Tr b ) )
2	1	cbvralvw	|- ( A. y e. N Tr y <-> A. b e. N Tr b )
3	2	bilani	|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N Tr b )
4		trss	|- ( Tr N -> ( b e. N -> b C_ N ) )
5		ssralv	|- ( b C_ N -> ( A. y e. N Tr y -> A. y e. b Tr y ) )
6	4 5	syl6	|- ( Tr N -> ( b e. N -> ( A. y e. N Tr y -> A. y e. b Tr y ) ) )
7	6	com23	|- ( Tr N -> ( A. y e. N Tr y -> ( b e. N -> A. y e. b Tr y ) ) )
8	7	imp	|- ( ( Tr N /\ A. y e. N Tr y ) -> ( b e. N -> A. y e. b Tr y ) )
9	8	ralrimiv	|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N A. y e. b Tr y )
10		r19.26	|- ( A. b e. N ( Tr b /\ A. y e. b Tr y ) <-> ( A. b e. N Tr b /\ A. b e. N A. y e. b Tr y ) )
11	3 9 10	sylanbrc	|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N ( Tr b /\ A. y e. b Tr y ) )