Theorem dford3lem1

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

	Ref	Expression
Assertion	dford3lem1	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑁 ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		treq	⊢ ( 𝑦 = 𝑏 → ( Tr 𝑦 ↔ Tr 𝑏 ) )
2	1	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ↔ ∀ 𝑏 ∈ 𝑁 Tr 𝑏 )
3	2	biimpi	⊢ ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 → ∀ 𝑏 ∈ 𝑁 Tr 𝑏 )
4	3	adantl	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑁 Tr 𝑏 )
5		trss	⊢ ( Tr 𝑁 → ( 𝑏 ∈ 𝑁 → 𝑏 ⊆ 𝑁 ) )
6		ssralv	⊢ ( 𝑏 ⊆ 𝑁 → ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
7	5 6	syl6	⊢ ( Tr 𝑁 → ( 𝑏 ∈ 𝑁 → ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) ) )
8	7	com23	⊢ ( Tr 𝑁 → ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 → ( 𝑏 ∈ 𝑁 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) ) )
9	8	imp	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ( 𝑏 ∈ 𝑁 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
10	9	ralrimiv	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑁 ∀ 𝑦 ∈ 𝑏 Tr 𝑦 )
11		r19.26	⊢ ( ∀ 𝑏 ∈ 𝑁 ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) ↔ ( ∀ 𝑏 ∈ 𝑁 Tr 𝑏 ∧ ∀ 𝑏 ∈ 𝑁 ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
12	4 10 11	sylanbrc	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑁 ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )