Metamath Proof Explorer

Theorem suceloniOLD

Description: Obsolete version of onsuc as of 30-Nov-2024. (Contributed by NM, 6-Jun-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suceloniOLD ⊢A∈On→suc⁡A∈On

Proof

Step Hyp Ref Expression
1 onelss ⊢A∈On→x∈A→x⊆A
2 velsn ⊢x∈A↔x=A
3 eqimss ⊢x=A→x⊆A
4 2 3 sylbi ⊢x∈A→x⊆A
5 4 a1i ⊢A∈On→x∈A→x⊆A
6 1 5 orim12d ⊢A∈On→x∈A∨x∈A→x⊆A∨x⊆A
7 df-suc ⊢suc⁡A=A∪A
8 7 eleq2i ⊢x∈suc⁡A↔x∈A∪A
9 elun ⊢x∈A∪A↔x∈A∨x∈A
10 8 9 bitr2i ⊢x∈A∨x∈A↔x∈suc⁡A
11 oridm ⊢x⊆A∨x⊆A↔x⊆A
12 6 10 11 3imtr3g ⊢A∈On→x∈suc⁡A→x⊆A
13 sssucid ⊢A⊆suc⁡A
14 sstr2 ⊢x⊆A→A⊆suc⁡A→x⊆suc⁡A
15 12 13 14 syl6mpi ⊢A∈On→x∈suc⁡A→x⊆suc⁡A
16 15 ralrimiv ⊢A∈On→∀x∈suc⁡Ax⊆suc⁡A
17 dftr3 ⊢Tr⁡suc⁡A↔∀x∈suc⁡Ax⊆suc⁡A
18 16 17 sylibr ⊢A∈On→Tr⁡suc⁡A
19 onss ⊢A∈On→A⊆On
20 snssi ⊢A∈On→A⊆On
21 19 20 unssd ⊢A∈On→A∪A⊆On
22 7 21 eqsstrid ⊢A∈On→suc⁡A⊆On
23 ordon ⊢Ord⁡On
24 trssord ⊢Tr⁡suc⁡A∧suc⁡A⊆On∧Ord⁡On→Ord⁡suc⁡A
25 24 3exp ⊢Tr⁡suc⁡A→suc⁡A⊆On→Ord⁡On→Ord⁡suc⁡A
26 23 25 mpii ⊢Tr⁡suc⁡A→suc⁡A⊆On→Ord⁡suc⁡A
27 18 22 26 sylc ⊢A∈On→Ord⁡suc⁡A
28 sucexg ⊢A∈On→suc⁡A∈V
29 elong ⊢suc⁡A∈V→suc⁡A∈On↔Ord⁡suc⁡A
30 28 29 syl ⊢A∈On→suc⁡A∈On↔Ord⁡suc⁡A
31 27 30 mpbird ⊢A∈On→suc⁡A∈On