Metamath Proof Explorer

Theorem dford3lem2

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

Ref Expression
Assertion dford3lem2 ⊢Tr⁡x∧∀y∈xTr⁡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→∃cTr⁡c∧x∈c
9 1 3 8 sylancl ⊢Tr⁡x→∃cTr⁡c∧x∈c
10 9 adantr ⊢Tr⁡x∧∀y∈xTr⁡y→∃cTr⁡c∧x∈c
11 simprl ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On∧Tr⁡a∧∀y∈aTr⁡y→Tr⁡a
12 dford3lem1 ⊢Tr⁡a∧∀y∈aTr⁡y→∀b∈aTr⁡b∧∀y∈bTr⁡y
13 ralim ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On→∀b∈aTr⁡b∧∀y∈bTr⁡y→∀b∈ab∈On
14 12 13 syl5 ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On→Tr⁡a∧∀y∈aTr⁡y→∀b∈ab∈On
15 14 imp ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On∧Tr⁡a∧∀y∈aTr⁡y→∀b∈ab∈On
16 dfss3 ⊢a⊆On↔∀b∈ab∈On
17 15 16 sylibr ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On∧Tr⁡a∧∀y∈aTr⁡y→a⊆On
18 ordon ⊢Ord⁡On
19 18 a1i ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On∧Tr⁡a∧∀y∈aTr⁡y→Ord⁡On
20 trssord ⊢Tr⁡a∧a⊆On∧Ord⁡On→Ord⁡a
21 11 17 19 20 syl3anc ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On∧Tr⁡a∧∀y∈aTr⁡y→Ord⁡a
22 vex ⊢a∈V
23 22 elon ⊢a∈On↔Ord⁡a
24 21 23 sylibr ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On∧Tr⁡a∧∀y∈aTr⁡y→a∈On
25 24 ex ⊢∀b∈aTr⁡b∧∀y∈bTr⁡y→b∈On→Tr⁡a∧∀y∈aTr⁡y→a∈On
26 treq ⊢a=b→Tr⁡a↔Tr⁡b
27 raleq ⊢a=b→∀y∈aTr⁡y↔∀y∈bTr⁡y
28 26 27 anbi12d ⊢a=b→Tr⁡a∧∀y∈aTr⁡y↔Tr⁡b∧∀y∈bTr⁡y
29 eleq1w ⊢a=b→a∈On↔b∈On
30 28 29 imbi12d ⊢a=b→Tr⁡a∧∀y∈aTr⁡y→a∈On↔Tr⁡b∧∀y∈bTr⁡y→b∈On
31 treq ⊢a=x→Tr⁡a↔Tr⁡x
32 raleq ⊢a=x→∀y∈aTr⁡y↔∀y∈xTr⁡y
33 31 32 anbi12d ⊢a=x→Tr⁡a∧∀y∈aTr⁡y↔Tr⁡x∧∀y∈xTr⁡y
34 eleq1w ⊢a=x→a∈On↔x∈On
35 33 34 imbi12d ⊢a=x→Tr⁡a∧∀y∈aTr⁡y→a∈On↔Tr⁡x∧∀y∈xTr⁡y→x∈On
36 25 30 35 setindtrs ⊢∃cTr⁡c∧x∈c→Tr⁡x∧∀y∈xTr⁡y→x∈On
37 10 36 mpcom ⊢Tr⁡x∧∀y∈xTr⁡y→x∈On