Metamath Proof Explorer


Theorem rankuni2b

Description: The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion rankuni2b AR1OnrankA=xArankx

Proof

Step Hyp Ref Expression
1 uniwf AR1OnAR1On
2 rankval3b AR1OnrankA=zOn|yArankyz
3 1 2 sylbi AR1OnrankA=zOn|yArankyz
4 eleq2 z=xArankxrankyzrankyxArankx
5 4 ralbidv z=xArankxyArankyzyArankyxArankx
6 iuneq1 y=Axyrankx=xArankx
7 6 eleq1d y=AxyrankxOnxArankxOn
8 vex yV
9 rankon rankxOn
10 9 rgenw xyrankxOn
11 iunon yVxyrankxOnxyrankxOn
12 8 10 11 mp2an xyrankxOn
13 7 12 vtoclg AR1OnxArankxOn
14 eluni2 yAxAyx
15 nfv xAR1On
16 nfiu1 _xxArankx
17 16 nfel2 xrankyxArankx
18 r1elssi AR1OnAR1On
19 18 sseld AR1OnxAxR1On
20 rankelb xR1Onyxrankyrankx
21 19 20 syl6 AR1OnxAyxrankyrankx
22 ssiun2 xArankxxArankx
23 22 sseld xArankyrankxrankyxArankx
24 23 a1i AR1OnxArankyrankxrankyxArankx
25 21 24 syldd AR1OnxAyxrankyxArankx
26 15 17 25 rexlimd AR1OnxAyxrankyxArankx
27 14 26 syl5bi AR1OnyArankyxArankx
28 27 ralrimiv AR1OnyArankyxArankx
29 5 13 28 elrabd AR1OnxArankxzOn|yArankyz
30 intss1 xArankxzOn|yArankyzzOn|yArankyzxArankx
31 29 30 syl AR1OnzOn|yArankyzxArankx
32 3 31 eqsstrd AR1OnrankAxArankx
33 1 biimpi AR1OnAR1On
34 elssuni xAxA
35 rankssb AR1OnxArankxrankA
36 33 34 35 syl2im AR1OnxArankxrankA
37 36 ralrimiv AR1OnxArankxrankA
38 iunss xArankxrankAxArankxrankA
39 37 38 sylibr AR1OnxArankxrankA
40 32 39 eqssd AR1OnrankA=xArankx