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	bilani	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑁 Tr 𝑏 )
4		trss	⊢ ( Tr 𝑁 → ( 𝑏 ∈ 𝑁 → 𝑏 ⊆ 𝑁 ) )
5		ssralv	⊢ ( 𝑏 ⊆ 𝑁 → ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
6	4 5	syl6	⊢ ( Tr 𝑁 → ( 𝑏 ∈ 𝑁 → ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) ) )
7	6	com23	⊢ ( Tr 𝑁 → ( ∀ 𝑦 ∈ 𝑁 Tr 𝑦 → ( 𝑏 ∈ 𝑁 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) ) )
8	7	imp	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ( 𝑏 ∈ 𝑁 → ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
9	8	ralrimiv	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑁 ∀ 𝑦 ∈ 𝑏 Tr 𝑦 )
10		r19.26	⊢ ( ∀ 𝑏 ∈ 𝑁 ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) ↔ ( ∀ 𝑏 ∈ 𝑁 Tr 𝑏 ∧ ∀ 𝑏 ∈ 𝑁 ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )
11	3 9 10	sylanbrc	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑦 ∈ 𝑁 Tr 𝑦 ) → ∀ 𝑏 ∈ 𝑁 ( Tr 𝑏 ∧ ∀ 𝑦 ∈ 𝑏 Tr 𝑦 ) )