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 biimpi ⊢ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N Tr ⁡ b
4 3 adantl ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N Tr ⁡ b
5 trss ⊢ Tr ⁡ N → b ∈ N → b ⊆ N
6 ssralv ⊢ b ⊆ N → ∀ y ∈ N Tr ⁡ y → ∀ y ∈ b Tr ⁡ y
7 5 6 syl6 ⊢ Tr ⁡ N → b ∈ N → ∀ y ∈ N Tr ⁡ y → ∀ y ∈ b Tr ⁡ y
8 7 com23 ⊢ Tr ⁡ N → ∀ y ∈ N Tr ⁡ y → b ∈ N → ∀ y ∈ b Tr ⁡ y
9 8 imp ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → b ∈ N → ∀ y ∈ b Tr ⁡ y
10 9 ralrimiv ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N ∀ y ∈ b Tr ⁡ y
11 r19.26 ⊢ ∀ b ∈ N Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y ↔ ∀ b ∈ N Tr ⁡ b ∧ ∀ b ∈ N ∀ y ∈ b Tr ⁡ y
12 4 10 11 sylanbrc ⊢ Tr ⁡ N ∧ ∀ y ∈ N Tr ⁡ y → ∀ b ∈ N Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y