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	biimpi	|- ( A. y e. N Tr y -> A. b e. N Tr b )
4	3	adantl	|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N Tr b )
5		trss	|- ( Tr N -> ( b e. N -> b C_ N ) )
6		ssralv	|- ( b C_ N -> ( A. y e. N Tr y -> A. y e. b Tr y ) )
7	5 6	syl6	|- ( Tr N -> ( b e. N -> ( A. y e. N Tr y -> A. y e. b Tr y ) ) )
8	7	com23	|- ( Tr N -> ( A. y e. N Tr y -> ( b e. N -> A. y e. b Tr y ) ) )
9	8	imp	|- ( ( Tr N /\ A. y e. N Tr y ) -> ( b e. N -> A. y e. b Tr y ) )
10	9	ralrimiv	|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N A. y e. b Tr y )
11		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 ) )
12	4 10 11	sylanbrc	|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N ( Tr b /\ A. y e. b Tr y ) )