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 ⁡ ⋃ A = ⋃ rank ⁡ A

Proof

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