Theorem dford3lem1 43679

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

Assertion

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

Distinct variable group:   𝑦,𝑏,𝑁

Proof of Theorem dford3lem1

Step	Hyp	Ref	Expression
1		treq 5229	. . . 4 ⊢ (𝑦 = 𝑏 → (Tr 𝑦 ↔ Tr 𝑏))
2	1	cbvralvw 3249	. . 3 ⊢ (∀𝑦 ∈ 𝑁 Tr 𝑦 ↔ ∀𝑏 ∈ 𝑁 Tr 𝑏)
3	2	bilani 509	. 2 ⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → ∀𝑏 ∈ 𝑁 Tr 𝑏)
4		trss 5232	. . . . . 6 ⊢ (Tr 𝑁 → (𝑏 ∈ 𝑁 → 𝑏 ⊆ 𝑁))
5		ssralv 4014	. . . . . 6 ⊢ (𝑏 ⊆ 𝑁 → (∀𝑦 ∈ 𝑁 Tr 𝑦 → ∀𝑦 ∈ 𝑏 Tr 𝑦))
6	4, 5	syl6 36	. . . . 5 ⊢ (Tr 𝑁 → (𝑏 ∈ 𝑁 → (∀𝑦 ∈ 𝑁 Tr 𝑦 → ∀𝑦 ∈ 𝑏 Tr 𝑦)))
7	6	com23 87	. . . 4 ⊢ (Tr 𝑁 → (∀𝑦 ∈ 𝑁 Tr 𝑦 → (𝑏 ∈ 𝑁 → ∀𝑦 ∈ 𝑏 Tr 𝑦)))
8	7	imp 411	. . 3 ⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → (𝑏 ∈ 𝑁 → ∀𝑦 ∈ 𝑏 Tr 𝑦))
9	8	ralrimiv 3162	. 2 ⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → ∀𝑏 ∈ 𝑁 ∀𝑦 ∈ 𝑏 Tr 𝑦)
10		r19.26 3131	. 2 ⊢ (∀𝑏 ∈ 𝑁 (Tr 𝑏 ∧ ∀𝑦 ∈ 𝑏 Tr 𝑦) ↔ (∀𝑏 ∈ 𝑁 Tr 𝑏 ∧ ∀𝑏 ∈ 𝑁 ∀𝑦 ∈ 𝑏 Tr 𝑦))
11	3, 9, 10	sylanbrc 594	1 ⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → ∀𝑏 ∈ 𝑁 (Tr 𝑏 ∧ ∀𝑦 ∈ 𝑏 Tr 𝑦))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085   ⊆ wss 3913  Tr wtr 5222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-v 3465  df-ss 3930  df-uni 4877  df-tr 5223

This theorem is referenced by:  dford3lem2  43680  dford3  43681