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 syl6eqr ⊢ ( ¬ 𝐴 ∈ 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 ‘ 𝐴 )