Metamath Proof Explorer


Theorem rankuni

Description: The rank of a union. Part of Exercise 4 of Kunen p. 107. (Contributed by NM, 15-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankuni ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 unieq ( 𝑥 = 𝐴 𝑥 = 𝐴 )
2 1 fveq2d ( 𝑥 = 𝐴 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
3 fveq2 ( 𝑥 = 𝐴 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
4 3 unieqd ( 𝑥 = 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
5 2 4 eqeq12d ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 ) ) )
6 vex 𝑥 ∈ V
7 6 rankuni2 ( rank ‘ 𝑥 ) = 𝑧𝑥 ( rank ‘ 𝑧 )
8 fvex ( rank ‘ 𝑧 ) ∈ V
9 8 dfiun2 𝑧𝑥 ( rank ‘ 𝑧 ) = { 𝑦 ∣ ∃ 𝑧𝑥 𝑦 = ( rank ‘ 𝑧 ) }
10 7 9 eqtri ( rank ‘ 𝑥 ) = { 𝑦 ∣ ∃ 𝑧𝑥 𝑦 = ( rank ‘ 𝑧 ) }
11 df-rex ( ∃ 𝑧𝑥 𝑦 = ( rank ‘ 𝑧 ) ↔ ∃ 𝑧 ( 𝑧𝑥𝑦 = ( rank ‘ 𝑧 ) ) )
12 6 rankel ( 𝑧𝑥 → ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑥 ) )
13 12 anim1i ( ( 𝑧𝑥𝑦 = ( rank ‘ 𝑧 ) ) → ( ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) )
14 13 eximi ( ∃ 𝑧 ( 𝑧𝑥𝑦 = ( rank ‘ 𝑧 ) ) → ∃ 𝑧 ( ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) )
15 19.42v ( ∃ 𝑧 ( 𝑦 ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) ↔ ( 𝑦 ∈ ( rank ‘ 𝑥 ) ∧ ∃ 𝑧 𝑦 = ( rank ‘ 𝑧 ) ) )
16 eleq1 ( 𝑦 = ( rank ‘ 𝑧 ) → ( 𝑦 ∈ ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑥 ) ) )
17 16 pm5.32ri ( ( 𝑦 ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) ↔ ( ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) )
18 17 exbii ( ∃ 𝑧 ( 𝑦 ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) ↔ ∃ 𝑧 ( ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) )
19 simpl ( ( 𝑦 ∈ ( rank ‘ 𝑥 ) ∧ ∃ 𝑧 𝑦 = ( rank ‘ 𝑧 ) ) → 𝑦 ∈ ( rank ‘ 𝑥 ) )
20 rankon ( rank ‘ 𝑥 ) ∈ On
21 20 oneli ( 𝑦 ∈ ( rank ‘ 𝑥 ) → 𝑦 ∈ On )
22 r1fnon 𝑅1 Fn On
23 fndm ( 𝑅1 Fn On → dom 𝑅1 = On )
24 22 23 ax-mp dom 𝑅1 = On
25 21 24 eleqtrrdi ( 𝑦 ∈ ( rank ‘ 𝑥 ) → 𝑦 ∈ dom 𝑅1 )
26 rankr1id ( 𝑦 ∈ dom 𝑅1 ↔ ( rank ‘ ( 𝑅1𝑦 ) ) = 𝑦 )
27 25 26 sylib ( 𝑦 ∈ ( rank ‘ 𝑥 ) → ( rank ‘ ( 𝑅1𝑦 ) ) = 𝑦 )
28 27 eqcomd ( 𝑦 ∈ ( rank ‘ 𝑥 ) → 𝑦 = ( rank ‘ ( 𝑅1𝑦 ) ) )
29 fvex ( 𝑅1𝑦 ) ∈ V
30 fveq2 ( 𝑧 = ( 𝑅1𝑦 ) → ( rank ‘ 𝑧 ) = ( rank ‘ ( 𝑅1𝑦 ) ) )
31 30 eqeq2d ( 𝑧 = ( 𝑅1𝑦 ) → ( 𝑦 = ( rank ‘ 𝑧 ) ↔ 𝑦 = ( rank ‘ ( 𝑅1𝑦 ) ) ) )
32 29 31 spcev ( 𝑦 = ( rank ‘ ( 𝑅1𝑦 ) ) → ∃ 𝑧 𝑦 = ( rank ‘ 𝑧 ) )
33 28 32 syl ( 𝑦 ∈ ( rank ‘ 𝑥 ) → ∃ 𝑧 𝑦 = ( rank ‘ 𝑧 ) )
34 33 ancli ( 𝑦 ∈ ( rank ‘ 𝑥 ) → ( 𝑦 ∈ ( rank ‘ 𝑥 ) ∧ ∃ 𝑧 𝑦 = ( rank ‘ 𝑧 ) ) )
35 19 34 impbii ( ( 𝑦 ∈ ( rank ‘ 𝑥 ) ∧ ∃ 𝑧 𝑦 = ( rank ‘ 𝑧 ) ) ↔ 𝑦 ∈ ( rank ‘ 𝑥 ) )
36 15 18 35 3bitr3i ( ∃ 𝑧 ( ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑥 ) ∧ 𝑦 = ( rank ‘ 𝑧 ) ) ↔ 𝑦 ∈ ( rank ‘ 𝑥 ) )
37 14 36 sylib ( ∃ 𝑧 ( 𝑧𝑥𝑦 = ( rank ‘ 𝑧 ) ) → 𝑦 ∈ ( rank ‘ 𝑥 ) )
38 11 37 sylbi ( ∃ 𝑧𝑥 𝑦 = ( rank ‘ 𝑧 ) → 𝑦 ∈ ( rank ‘ 𝑥 ) )
39 38 abssi { 𝑦 ∣ ∃ 𝑧𝑥 𝑦 = ( rank ‘ 𝑧 ) } ⊆ ( rank ‘ 𝑥 )
40 39 unissi { 𝑦 ∣ ∃ 𝑧𝑥 𝑦 = ( rank ‘ 𝑧 ) } ⊆ ( rank ‘ 𝑥 )
41 10 40 eqsstri ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑥 )
42 pwuni 𝑥 ⊆ 𝒫 𝑥
43 vuniex 𝑥 ∈ V
44 43 pwex 𝒫 𝑥 ∈ V
45 44 rankss ( 𝑥 ⊆ 𝒫 𝑥 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝒫 𝑥 ) )
46 42 45 ax-mp ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝒫 𝑥 )
47 43 rankpw ( rank ‘ 𝒫 𝑥 ) = suc ( rank ‘ 𝑥 )
48 46 47 sseqtri ( rank ‘ 𝑥 ) ⊆ suc ( rank ‘ 𝑥 )
49 48 unissi ( rank ‘ 𝑥 ) ⊆ suc ( rank ‘ 𝑥 )
50 rankon ( rank ‘ 𝑥 ) ∈ On
51 50 onunisuci suc ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 )
52 49 51 sseqtri ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑥 )
53 41 52 eqssi ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 )
54 5 53 vtoclg ( 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 ) )
55 uniexb ( 𝐴 ∈ V ↔ 𝐴 ∈ V )
56 fvprc ( ¬ 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ∅ )
57 55 56 sylnbi ( ¬ 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ∅ )
58 uni0 ∅ = ∅
59 57 58 eqtr4di ( ¬ 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ∅ )
60 fvprc ( ¬ 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ∅ )
61 60 unieqd ( ¬ 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ∅ )
62 59 61 eqtr4d ( ¬ 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 ) )
63 54 62 pm2.61i ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 )