Step |
Hyp |
Ref |
Expression |
1 |
|
unwf |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) ) |
2 |
|
rankval3b |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ∩ { 𝑦 ∈ On ∣ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 } ) |
3 |
1 2
|
sylbi |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ∩ { 𝑦 ∈ On ∣ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 } ) |
4 |
3
|
eleq2d |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝑥 ∈ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ 𝑥 ∈ ∩ { 𝑦 ∈ On ∣ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 } ) ) |
5 |
|
vex |
⊢ 𝑥 ∈ V |
6 |
5
|
elintrab |
⊢ ( 𝑥 ∈ ∩ { 𝑦 ∈ On ∣ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 } ↔ ∀ 𝑦 ∈ On ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 → 𝑥 ∈ 𝑦 ) ) |
7 |
4 6
|
bitrdi |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝑥 ∈ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ∀ 𝑦 ∈ On ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 → 𝑥 ∈ 𝑦 ) ) ) |
8 |
|
elun |
⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) |
9 |
|
rankelb |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) ) |
10 |
|
elun1 |
⊢ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) → ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) |
11 |
9 10
|
syl6 |
⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
12 |
|
rankelb |
⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐵 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐵 ) ) ) |
13 |
|
elun2 |
⊢ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) |
14 |
12 13
|
syl6 |
⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐵 → ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
15 |
11 14
|
jaao |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
16 |
8 15
|
syl5bi |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
17 |
16
|
ralrimiv |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) |
18 |
|
rankon |
⊢ ( rank ‘ 𝐴 ) ∈ On |
19 |
|
rankon |
⊢ ( rank ‘ 𝐵 ) ∈ On |
20 |
18 19
|
onun2i |
⊢ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ On |
21 |
|
eleq2 |
⊢ ( 𝑦 = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( ( rank ‘ 𝑥 ) ∈ 𝑦 ↔ ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
22 |
21
|
ralbidv |
⊢ ( 𝑦 = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 ↔ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
23 |
|
eleq2 |
⊢ ( 𝑦 = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
24 |
22 23
|
imbi12d |
⊢ ( 𝑦 = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → ( ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 → 𝑥 ∈ 𝑦 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → 𝑥 ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) ) |
25 |
24
|
rspcv |
⊢ ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ∈ On → ( ∀ 𝑦 ∈ On ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 → 𝑥 ∈ 𝑦 ) → ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → 𝑥 ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) ) |
26 |
20 25
|
ax-mp |
⊢ ( ∀ 𝑦 ∈ On ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 → 𝑥 ∈ 𝑦 ) → ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → 𝑥 ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
27 |
17 26
|
syl5com |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( ∀ 𝑦 ∈ On ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( rank ‘ 𝑥 ) ∈ 𝑦 → 𝑥 ∈ 𝑦 ) → 𝑥 ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
28 |
7 27
|
sylbid |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝑥 ∈ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) → 𝑥 ∈ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) ) |
29 |
28
|
ssrdv |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) |
30 |
|
ssun1 |
⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) |
31 |
|
rankssb |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) |
32 |
30 31
|
mpi |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) |
33 |
|
ssun2 |
⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) |
34 |
|
rankssb |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) → ( rank ‘ 𝐵 ) ⊆ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) |
35 |
33 34
|
mpi |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐵 ) ⊆ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) |
36 |
32 35
|
unssd |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ⊆ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) |
37 |
1 36
|
sylbi |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ⊆ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) |
38 |
29 37
|
eqssd |
⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) ) |