Metamath Proof Explorer

Theorem dford3lem2

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

Ref Expression
Assertion dford3lem2 ⊢ Tr ⁡ x ∧ ∀ y ∈ x Tr ⁡ y → x ∈ On

Proof

Step Hyp Ref Expression
1 suctr ⊢ Tr ⁡ x → Tr ⁡ suc ⁡ x
2 vex ⊢ x ∈ V
3 2 sucid ⊢ x ∈ suc ⁡ x
4 2 sucex ⊢ suc ⁡ x ∈ V
5 treq ⊢ c = suc ⁡ x → Tr ⁡ c ↔ Tr ⁡ suc ⁡ x
6 eleq2 ⊢ c = suc ⁡ x → x ∈ c ↔ x ∈ suc ⁡ x
7 5 6 anbi12d ⊢ c = suc ⁡ x → Tr ⁡ c ∧ x ∈ c ↔ Tr ⁡ suc ⁡ x ∧ x ∈ suc ⁡ x
8 4 7 spcev ⊢ Tr ⁡ suc ⁡ x ∧ x ∈ suc ⁡ x → ∃ c Tr ⁡ c ∧ x ∈ c
9 1 3 8 sylancl ⊢ Tr ⁡ x → ∃ c Tr ⁡ c ∧ x ∈ c
10 9 adantr ⊢ Tr ⁡ x ∧ ∀ y ∈ x Tr ⁡ y → ∃ c Tr ⁡ c ∧ x ∈ c
11 simprl ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On ∧ Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → Tr ⁡ a
12 dford3lem1 ⊢ Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y
13 ralim ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On → ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → ∀ b ∈ a b ∈ On
14 12 13 syl5 ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On → Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → ∀ b ∈ a b ∈ On
15 14 imp ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On ∧ Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → ∀ b ∈ a b ∈ On
16 dfss3 ⊢ a ⊆ On ↔ ∀ b ∈ a b ∈ On
17 15 16 sylibr ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On ∧ Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → a ⊆ On
18 ordon ⊢ Ord ⁡ On
19 18 a1i ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On ∧ Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → Ord ⁡ On
20 trssord ⊢ Tr ⁡ a ∧ a ⊆ On ∧ Ord ⁡ On → Ord ⁡ a
21 11 17 19 20 syl3anc ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On ∧ Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → Ord ⁡ a
22 vex ⊢ a ∈ V
23 22 elon ⊢ a ∈ On ↔ Ord ⁡ a
24 21 23 sylibr ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On ∧ Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → a ∈ On
25 24 ex ⊢ ∀ b ∈ a Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On → Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → a ∈ On
26 treq ⊢ a = b → Tr ⁡ a ↔ Tr ⁡ b
27 raleq ⊢ a = b → ∀ y ∈ a Tr ⁡ y ↔ ∀ y ∈ b Tr ⁡ y
28 26 27 anbi12d ⊢ a = b → Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y ↔ Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y
29 eleq1w ⊢ a = b → a ∈ On ↔ b ∈ On
30 28 29 imbi12d ⊢ a = b → Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → a ∈ On ↔ Tr ⁡ b ∧ ∀ y ∈ b Tr ⁡ y → b ∈ On
31 treq ⊢ a = x → Tr ⁡ a ↔ Tr ⁡ x
32 raleq ⊢ a = x → ∀ y ∈ a Tr ⁡ y ↔ ∀ y ∈ x Tr ⁡ y
33 31 32 anbi12d ⊢ a = x → Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y ↔ Tr ⁡ x ∧ ∀ y ∈ x Tr ⁡ y
34 eleq1w ⊢ a = x → a ∈ On ↔ x ∈ On
35 33 34 imbi12d ⊢ a = x → Tr ⁡ a ∧ ∀ y ∈ a Tr ⁡ y → a ∈ On ↔ Tr ⁡ x ∧ ∀ y ∈ x Tr ⁡ y → x ∈ On
36 25 30 35 setindtrs ⊢ ∃ c Tr ⁡ c ∧ x ∈ c → Tr ⁡ x ∧ ∀ y ∈ x Tr ⁡ y → x ∈ On
37 10 36 mpcom ⊢ Tr ⁡ x ∧ ∀ y ∈ x Tr ⁡ y → x ∈ On