Metamath Proof Explorer

Theorem dford3lem1

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

Ref Expression
Assertion dford3lem1 ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y

Proof

Step Hyp Ref Expression
1 treq ⊢ y = b → Tr ⁡ y ↔ Tr ⁡ b
2 1 cbvralvw ⊢ ∀ y ∈ N Tr ⁡ y ↔ ∀ b ∈ N Tr ⁡ b
3 2 bilani ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N Tr ⁡ b
4 trss ⊢ Tr ⁡ N → b ∈ N → b ⊆ N
5 ssralv ⊢ b ⊆ N → ∀ y ∈ N Tr ⁡ y → ∀ y ∈ b Tr ⁡ y
6 4 5 syl6 ⊢ Tr ⁡ N → b ∈ N → ∀ y ∈ N Tr ⁡ y → ∀ y ∈ b Tr ⁡ y
7 6 com23 ⊢ Tr ⁡ N → ∀ y ∈ N Tr ⁡ y → b ∈ N → ∀ y ∈ b Tr ⁡ y
8 7 imp ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → b ∈ N → ∀ y ∈ b Tr ⁡ y
9 8 ralrimiv ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N ∀ y ∈ b Tr ⁡ y
10 r19.26 ⊢ ∀ b ∈ N Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y ↔ ∀ b ∈ N Tr ⁡ b ∧ ∀ b ∈ N ∀ y ∈ b Tr ⁡ y
11 3 9 10 sylanbrc ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y