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 \to ⋃ x = ⋃ A$
2	1	fveq2d	$⊢ x = A \to rank (⋃ x) = rank (⋃ A)$
3		fveq2	$⊢ x = A \to rank (x) = rank (A)$
4	3	unieqd	$⊢ x = A \to ⋃ rank (x) = ⋃ rank (A)$
5	2 4	eqeq12d	$⊢ x = A \to (rank (⋃ x) = ⋃ rank (x) \leftrightarrow rank (⋃ A) = ⋃ rank (A))$
6		vex	$⊢ x \in V$
7	6	rankuni2	$⊢ rank (⋃ x) = ⋃_{z \in x} rank (z)$
8		fvex	$⊢ rank (z) \in V$
9	8	dfiun2	$⊢ ⋃_{z \in x} rank (z) = ⋃ \{y \| \exists z \in x y = rank (z)\}$
10	7 9	eqtri	$⊢ rank (⋃ x) = ⋃ \{y \| \exists z \in x y = rank (z)\}$
11		df-rex	$⊢ \exists z \in x y = rank (z) \leftrightarrow \exists z (z \in x \land y = rank (z))$
12	6	rankel	$⊢ z \in x \to rank (z) \in rank (x)$
13	12	anim1i	$⊢ (z \in x \land y = rank (z)) \to (rank (z) \in rank (x) \land y = rank (z))$
14	13	eximi	$⊢ \exists z (z \in x \land y = rank (z)) \to \exists z (rank (z) \in rank (x) \land y = rank (z))$
15		19.42v	$⊢ \exists z (y \in rank (x) \land y = rank (z)) \leftrightarrow (y \in rank (x) \land \exists z y = rank (z))$
16		eleq1	$⊢ y = rank (z) \to (y \in rank (x) \leftrightarrow rank (z) \in rank (x))$
17	16	pm5.32ri	$⊢ (y \in rank (x) \land y = rank (z)) \leftrightarrow (rank (z) \in rank (x) \land y = rank (z))$
18	17	exbii	$⊢ \exists z (y \in rank (x) \land y = rank (z)) \leftrightarrow \exists z (rank (z) \in rank (x) \land y = rank (z))$
19		simpl	$⊢ (y \in rank (x) \land \exists z y = rank (z)) \to y \in rank (x)$
20		rankon	$⊢ rank (x) \in On$
21	20	oneli	$⊢ y \in rank (x) \to y \in On$
22		r1fnon	$⊢ R_{1} Fn On$
23		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
24	22 23	ax-mp	$⊢ dom R_{1} = On$
25	21 24	eleqtrrdi	$⊢ y \in rank (x) \to y \in dom R_{1}$
26		rankr1id	$⊢ y \in dom R_{1} \leftrightarrow rank (R_{1} (y)) = y$
27	25 26	sylib	$⊢ y \in rank (x) \to rank (R_{1} (y)) = y$
28	27	eqcomd	$⊢ y \in rank (x) \to y = rank (R_{1} (y))$
29		fvex	$⊢ R_{1} (y) \in V$
30		fveq2	$⊢ z = R_{1} (y) \to rank (z) = rank (R_{1} (y))$
31	30	eqeq2d	$⊢ z = R_{1} (y) \to (y = rank (z) \leftrightarrow y = rank (R_{1} (y)))$
32	29 31	spcev	$⊢ y = rank (R_{1} (y)) \to \exists z y = rank (z)$
33	28 32	syl	$⊢ y \in rank (x) \to \exists z y = rank (z)$
34	33	ancli	$⊢ y \in rank (x) \to (y \in rank (x) \land \exists z y = rank (z))$
35	19 34	impbii	$⊢ (y \in rank (x) \land \exists z y = rank (z)) \leftrightarrow y \in rank (x)$
36	15 18 35	3bitr3i	$⊢ \exists z (rank (z) \in rank (x) \land y = rank (z)) \leftrightarrow y \in rank (x)$
37	14 36	sylib	$⊢ \exists z (z \in x \land y = rank (z)) \to y \in rank (x)$
38	11 37	sylbi	$⊢ \exists z \in x y = rank (z) \to y \in rank (x)$
39	38	abssi	$⊢ \{y \| \exists z \in x y = rank (z)\} \subseteq rank (x)$
40	39	unissi	$⊢ ⋃ \{y \| \exists z \in x y = rank (z)\} \subseteq ⋃ rank (x)$
41	10 40	eqsstri	$⊢ rank (⋃ x) \subseteq ⋃ rank (x)$
42		pwuni	$⊢ x \subseteq 𝒫 ⋃ x$
43		vuniex	$⊢ ⋃ x \in V$
44	43	pwex	$⊢ 𝒫 ⋃ x \in V$
45	44	rankss	$⊢ x \subseteq 𝒫 ⋃ x \to rank (x) \subseteq rank (𝒫 ⋃ x)$
46	42 45	ax-mp	$⊢ rank (x) \subseteq rank (𝒫 ⋃ x)$
47	43	rankpw	$⊢ rank (𝒫 ⋃ x) = suc rank (⋃ x)$
48	46 47	sseqtri	$⊢ rank (x) \subseteq suc rank (⋃ x)$
49	48	unissi	$⊢ ⋃ rank (x) \subseteq ⋃ suc rank (⋃ x)$
50		rankon	$⊢ rank (⋃ x) \in On$
51	50	onunisuci	$⊢ ⋃ suc rank (⋃ x) = rank (⋃ x)$
52	49 51	sseqtri	$⊢ ⋃ rank (x) \subseteq rank (⋃ x)$
53	41 52	eqssi	$⊢ rank (⋃ x) = ⋃ rank (x)$
54	5 53	vtoclg	$⊢ A \in V \to rank (⋃ A) = ⋃ rank (A)$
55		uniexb	$⊢ A \in V \leftrightarrow ⋃ A \in V$
56		fvprc	$⊢ \neg ⋃ A \in V \to rank (⋃ A) = \emptyset$
57	55 56	sylnbi	$⊢ \neg A \in V \to rank (⋃ A) = \emptyset$
58		uni0	$⊢ ⋃ \emptyset = \emptyset$
59	57 58	eqtr4di	$⊢ \neg A \in V \to rank (⋃ A) = ⋃ \emptyset$
60		fvprc	$⊢ \neg A \in V \to rank (A) = \emptyset$
61	60	unieqd	$⊢ \neg A \in V \to ⋃ rank (A) = ⋃ \emptyset$
62	59 61	eqtr4d	$⊢ \neg A \in V \to rank (⋃ A) = ⋃ rank (A)$
63	54 62	pm2.61i	$⊢ rank (⋃ A) = ⋃ rank (A)$

Metamath Proof Explorer

Theorem rankuni

Proof