Metamath Proof Explorer

Theorem dford3lem1

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

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

Proof

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