Proof of Theorem hfun
Step | Hyp | Ref
| Expression |
1 | | rankung 31443 |
. . 3
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) →
(rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵))) |
2 | | elhf2g 31453 |
. . . . 5
⊢ (𝐴 ∈ Hf → (𝐴 ∈ Hf ↔
(rank‘𝐴) ∈
ω)) |
3 | 2 | ibi 255 |
. . . 4
⊢ (𝐴 ∈ Hf →
(rank‘𝐴) ∈
ω) |
4 | | elhf2g 31453 |
. . . . 5
⊢ (𝐵 ∈ Hf → (𝐵 ∈ Hf ↔
(rank‘𝐵) ∈
ω)) |
5 | 4 | ibi 255 |
. . . 4
⊢ (𝐵 ∈ Hf →
(rank‘𝐵) ∈
ω) |
6 | | eleq1a 2683 |
. . . . . 6
⊢
((rank‘𝐵)
∈ ω → (((rank‘𝐴) ∪ (rank‘𝐵)) = (rank‘𝐵) → ((rank‘𝐴) ∪ (rank‘𝐵)) ∈ ω)) |
7 | 6 | adantl 481 |
. . . . 5
⊢
(((rank‘𝐴)
∈ ω ∧ (rank‘𝐵) ∈ ω) → (((rank‘𝐴) ∪ (rank‘𝐵)) = (rank‘𝐵) → ((rank‘𝐴) ∪ (rank‘𝐵)) ∈
ω)) |
8 | | uncom 3719 |
. . . . . . . . . 10
⊢
((rank‘𝐵)
∪ (rank‘𝐴)) =
((rank‘𝐴) ∪
(rank‘𝐵)) |
9 | 8 | eqeq1i 2615 |
. . . . . . . . 9
⊢
(((rank‘𝐵)
∪ (rank‘𝐴)) =
(rank‘𝐴) ↔
((rank‘𝐴) ∪
(rank‘𝐵)) =
(rank‘𝐴)) |
10 | 9 | biimpi 205 |
. . . . . . . 8
⊢
(((rank‘𝐵)
∪ (rank‘𝐴)) =
(rank‘𝐴) →
((rank‘𝐴) ∪
(rank‘𝐵)) =
(rank‘𝐴)) |
11 | 10 | eleq1d 2672 |
. . . . . . 7
⊢
(((rank‘𝐵)
∪ (rank‘𝐴)) =
(rank‘𝐴) →
(((rank‘𝐴) ∪
(rank‘𝐵)) ∈
ω ↔ (rank‘𝐴) ∈ ω)) |
12 | 11 | biimprcd 239 |
. . . . . 6
⊢
((rank‘𝐴)
∈ ω → (((rank‘𝐵) ∪ (rank‘𝐴)) = (rank‘𝐴) → ((rank‘𝐴) ∪ (rank‘𝐵)) ∈ ω)) |
13 | 12 | adantr 480 |
. . . . 5
⊢
(((rank‘𝐴)
∈ ω ∧ (rank‘𝐵) ∈ ω) → (((rank‘𝐵) ∪ (rank‘𝐴)) = (rank‘𝐴) → ((rank‘𝐴) ∪ (rank‘𝐵)) ∈
ω)) |
14 | | nnord 6965 |
. . . . . . 7
⊢
((rank‘𝐴)
∈ ω → Ord (rank‘𝐴)) |
15 | | nnord 6965 |
. . . . . . 7
⊢
((rank‘𝐵)
∈ ω → Ord (rank‘𝐵)) |
16 | | ordtri2or2 5740 |
. . . . . . 7
⊢ ((Ord
(rank‘𝐴) ∧ Ord
(rank‘𝐵)) →
((rank‘𝐴) ⊆
(rank‘𝐵) ∨
(rank‘𝐵) ⊆
(rank‘𝐴))) |
17 | 14, 15, 16 | syl2an 493 |
. . . . . 6
⊢
(((rank‘𝐴)
∈ ω ∧ (rank‘𝐵) ∈ ω) → ((rank‘𝐴) ⊆ (rank‘𝐵) ∨ (rank‘𝐵) ⊆ (rank‘𝐴))) |
18 | | ssequn1 3745 |
. . . . . . 7
⊢
((rank‘𝐴)
⊆ (rank‘𝐵)
↔ ((rank‘𝐴)
∪ (rank‘𝐵)) =
(rank‘𝐵)) |
19 | | ssequn1 3745 |
. . . . . . 7
⊢
((rank‘𝐵)
⊆ (rank‘𝐴)
↔ ((rank‘𝐵)
∪ (rank‘𝐴)) =
(rank‘𝐴)) |
20 | 18, 19 | orbi12i 542 |
. . . . . 6
⊢
(((rank‘𝐴)
⊆ (rank‘𝐵) ∨
(rank‘𝐵) ⊆
(rank‘𝐴)) ↔
(((rank‘𝐴) ∪
(rank‘𝐵)) =
(rank‘𝐵) ∨
((rank‘𝐵) ∪
(rank‘𝐴)) =
(rank‘𝐴))) |
21 | 17, 20 | sylib 207 |
. . . . 5
⊢
(((rank‘𝐴)
∈ ω ∧ (rank‘𝐵) ∈ ω) → (((rank‘𝐴) ∪ (rank‘𝐵)) = (rank‘𝐵) ∨ ((rank‘𝐵) ∪ (rank‘𝐴)) = (rank‘𝐴))) |
22 | 7, 13, 21 | mpjaod 395 |
. . . 4
⊢
(((rank‘𝐴)
∈ ω ∧ (rank‘𝐵) ∈ ω) → ((rank‘𝐴) ∪ (rank‘𝐵)) ∈
ω) |
23 | 3, 5, 22 | syl2an 493 |
. . 3
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) →
((rank‘𝐴) ∪
(rank‘𝐵)) ∈
ω) |
24 | 1, 23 | eqeltrd 2688 |
. 2
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) →
(rank‘(𝐴 ∪ 𝐵)) ∈
ω) |
25 | | unexg 6857 |
. . 3
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ 𝐵) ∈ V) |
26 | | elhf2g 31453 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ∈ V → ((𝐴 ∪ 𝐵) ∈ Hf ↔ (rank‘(𝐴 ∪ 𝐵)) ∈ ω)) |
27 | 25, 26 | syl 17 |
. 2
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ((𝐴 ∪ 𝐵) ∈ Hf ↔ (rank‘(𝐴 ∪ 𝐵)) ∈ ω)) |
28 | 24, 27 | mpbird 246 |
1
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ 𝐵) ∈ Hf ) |