Theorem rankun 4701

Description: The rank of the union of two sets. Theorem 15.17(iii) of [Monk1] p. 112.

Hypotheses

Ref	Expression
rankun.1	⊢ A ∈ V
rankun.2	⊢ B ∈ V

Assertion

Ref	Expression
rankun	⊢ (rank ‘(A ∪ B)) = ((rank ‘A) ∪ (rank ‘B))

Proof of Theorem rankun

Step	Hyp	Ref	Expression
1		rankun.1	. . . . . . . 8 ⊢ A ∈ V
2		rankun.2	. . . . . . . 8 ⊢ B ∈ V
3	1, 2	unex 2878	. . . . . . 7 ⊢ (A ∪ B) ∈ V
4	3	rankval3 4691	. . . . . 6 ⊢ (rank ‘(A ∪ B)) = ∩{y ∈ On∣∀z ∈ (A ∪ B)(rank ‘z) ∈ y}
5	4	eleq2i 1541	. . . . 5 ⊢ (x ∈ (rank ‘(A ∪ B)) ↔ x ∈ ∩{y ∈ On∣∀z ∈ (A ∪ B)(rank ‘z) ∈ y})
6		visset 1816	. . . . . 6 ⊢ x ∈ V
7	6	elintrab 2549	. . . . 5 ⊢ (x ∈ ∩{y ∈ On∣∀z ∈ (A ∪ B)(rank ‘z) ∈ y} ↔ ∀y ∈ On (∀z ∈ (A ∪ B)(rank ‘z) ∈ y → x ∈ y))
8	5, 7	bitr 173	. . . 4 ⊢ (x ∈ (rank ‘(A ∪ B)) ↔ ∀y ∈ On (∀z ∈ (A ∪ B)(rank ‘z) ∈ y → x ∈ y))
9		elun 2176	. . . . . . 7 ⊢ (z ∈ (A ∪ B) ↔ (z ∈ A ⋁ z ∈ B))
10	1	rankel 4690	. . . . . . . . 9 ⊢ (z ∈ A → (rank ‘z) ∈ (rank ‘A))
11		elun1 2200	. . . . . . . . 9 ⊢ ((rank ‘z) ∈ (rank ‘A) → (rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)))
12	10, 11	syl 10	. . . . . . . 8 ⊢ (z ∈ A → (rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)))
13	2	rankel 4690	. . . . . . . . 9 ⊢ (z ∈ B → (rank ‘z) ∈ (rank ‘B))
14		elun2 2201	. . . . . . . . 9 ⊢ ((rank ‘z) ∈ (rank ‘B) → (rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)))
15	13, 14	syl 10	. . . . . . . 8 ⊢ (z ∈ B → (rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)))
16	12, 15	jaoi 341	. . . . . . 7 ⊢ ((z ∈ A ⋁ z ∈ B) → (rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)))
17	9, 16	sylbi 199	. . . . . 6 ⊢ (z ∈ (A ∪ B) → (rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)))
18	17	rgen 1701	. . . . 5 ⊢ ∀z ∈ (A ∪ B)(rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B))
19		rankon 4681	. . . . . . 7 ⊢ (rank ‘A) ∈ On
20		rankon 4681	. . . . . . 7 ⊢ (rank ‘B) ∈ On
21	19, 20	onun 3116	. . . . . 6 ⊢ ((rank ‘A) ∪ (rank ‘B)) ∈ On
22		eleq2 1538	. . . . . . . . 9 ⊢ (y = ((rank ‘A) ∪ (rank ‘B)) → ((rank ‘z) ∈ y ↔ (rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B))))
23	22	ralbidv 1666	. . . . . . . 8 ⊢ (y = ((rank ‘A) ∪ (rank ‘B)) → (∀z ∈ (A ∪ B)(rank ‘z) ∈ y ↔ ∀z ∈ (A ∪ B)(rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B))))
24		eleq2 1538	. . . . . . . 8 ⊢ (y = ((rank ‘A) ∪ (rank ‘B)) → (x ∈ y ↔ x ∈ ((rank ‘A) ∪ (rank ‘B))))
25	23, 24	imbi12d 628	. . . . . . 7 ⊢ (y = ((rank ‘A) ∪ (rank ‘B)) → ((∀z ∈ (A ∪ B)(rank ‘z) ∈ y → x ∈ y) ↔ (∀z ∈ (A ∪ B)(rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)) → x ∈ ((rank ‘A) ∪ (rank ‘B)))))
26	25	rcla4v 1876	. . . . . 6 ⊢ (((rank ‘A) ∪ (rank ‘B)) ∈ On → (∀y ∈ On (∀z ∈ (A ∪ B)(rank ‘z) ∈ y → x ∈ y) → (∀z ∈ (A ∪ B)(rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)) → x ∈ ((rank ‘A) ∪ (rank ‘B)))))
27	21, 26	ax-mp 7	. . . . 5 ⊢ (∀y ∈ On (∀z ∈ (A ∪ B)(rank ‘z) ∈ y → x ∈ y) → (∀z ∈ (A ∪ B)(rank ‘z) ∈ ((rank ‘A) ∪ (rank ‘B)) → x ∈ ((rank ‘A) ∪ (rank ‘B))))
28	18, 27	mpi 44	. . . 4 ⊢ (∀y ∈ On (∀z ∈ (A ∪ B)(rank ‘z) ∈ y → x ∈ y) → x ∈ ((rank ‘A) ∪ (rank ‘B)))
29	8, 28	sylbi 199	. . 3 ⊢ (x ∈ (rank ‘(A ∪ B)) → x ∈ ((rank ‘A) ∪ (rank ‘B)))
30	29	ssriv 2072	. 2 ⊢ (rank ‘(A ∪ B)) ⊆ ((rank ‘A) ∪ (rank ‘B))
31		ssun1 2196	. . . 4 ⊢ A ⊆ (A ∪ B)
32	3	rankss 4698	. . . 4 ⊢ (A ⊆ (A ∪ B) → (rank ‘A) ⊆ (rank ‘(A ∪ B)))
33	31, 32	ax-mp 7	. . 3 ⊢ (rank ‘A) ⊆ (rank ‘(A ∪ B))
34		ssun2 2197	. . . 4 ⊢ B ⊆ (A ∪ B)
35	3	rankss 4698	. . . 4 ⊢ (B ⊆ (A ∪ B) → (rank ‘B) ⊆ (rank ‘(A ∪ B)))
36	34, 35	ax-mp 7	. . 3 ⊢ (rank ‘B) ⊆ (rank ‘(A ∪ B))
37	33, 36	unssi 2208	. 2 ⊢ ((rank ‘A) ∪ (rank ‘B)) ⊆ (rank ‘(A ∪ B))
38	30, 37	eqssi 2081	1 ⊢ (rank ‘(A ∪ B)) = ((rank ‘A) ∪ (rank ‘B))

Syntax hints:   → wi 3   ⋁ wo 222   = wceq 958   ∈ wcel 960  ∀wral 1648  {crab 1651  Vcvv 1814   ∪ cun 2048   ⊆ wss 2050  ∩cint 2537  Oncon0 2954   ‘cfv 3188  rankcrnk 4652

This theorem is referenced by:  rankpr 4702  rankop 4703  ranksuc 4710  rankelun 4717  rankelpr 4718

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-reg 4602  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-rab 1655  df-v 1815  df-sbc 1945  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-fv 3204  df-rdg 3938  df-r1 4653  df-rank 4654

Copyright terms: Public domain