Theorem rankung

Description: The rank of the union of two sets. Closed form of rankun . (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	rankung	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uneq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∪ 𝑦 ) = ( 𝐴 ∪ 𝑦 ) )
2	1	fveq2d	⊢ ( 𝑥 = 𝐴 → ( rank ‘ ( 𝑥 ∪ 𝑦 ) ) = ( rank ‘ ( 𝐴 ∪ 𝑦 ) ) )
3		fveq2	⊢ ( 𝑥 = 𝐴 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
4	3	uneq1d	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝑦 ) ) )
5	2 4	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ ( 𝑥 ∪ 𝑦 ) ) = ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) ) ↔ ( rank ‘ ( 𝐴 ∪ 𝑦 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝑦 ) ) ) )
6		uneq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∪ 𝑦 ) = ( 𝐴 ∪ 𝐵 ) )
7	6	fveq2d	⊢ ( 𝑦 = 𝐵 → ( rank ‘ ( 𝐴 ∪ 𝑦 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
8		fveq2	⊢ ( 𝑦 = 𝐵 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐵 ) )
9	8	uneq2d	⊢ ( 𝑦 = 𝐵 → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝑦 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
10	7 9	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ( rank ‘ ( 𝐴 ∪ 𝑦 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝑦 ) ) ↔ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) )
11		vex	⊢ 𝑥 ∈ V
12		vex	⊢ 𝑦 ∈ V
13	11 12	rankun	⊢ ( rank ‘ ( 𝑥 ∪ 𝑦 ) ) = ( ( rank ‘ 𝑥 ) ∪ ( rank ‘ 𝑦 ) )
14	5 10 13	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )