Proof of Theorem nobndlem2
Step | Hyp | Ref
| Expression |
1 | | nobndlem2.2 |
. 2
⊢ 𝐶 = ∩
{𝑎 ∈ On ∣
∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋} |
2 | | nobndlem1 31091 |
. . . 4
⊢ (𝐹 ∈ 𝐴 → suc ∪
( bday “ 𝐹) ∈ On) |
3 | | ssel2 3563 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → 𝑛 ∈
No ) |
4 | | bdaydm 31077 |
. . . . . . . . . 10
⊢ dom bday = No
|
5 | 3, 4 | syl6eleqr 2699 |
. . . . . . . . 9
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → 𝑛 ∈ dom bday ) |
6 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → 𝑛 ∈ 𝐹) |
7 | | bdayfun 31075 |
. . . . . . . . . 10
⊢ Fun bday |
8 | | funfvima 6396 |
. . . . . . . . . 10
⊢ ((Fun
bday ∧ 𝑛 ∈ dom bday
) → (𝑛 ∈
𝐹 → ( bday ‘𝑛) ∈ ( bday
“ 𝐹))) |
9 | 7, 8 | mpan 702 |
. . . . . . . . 9
⊢ (𝑛 ∈ dom bday → (𝑛 ∈ 𝐹 → ( bday
‘𝑛) ∈
( bday “ 𝐹))) |
10 | 5, 6, 9 | sylc 63 |
. . . . . . . 8
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → ( bday ‘𝑛) ∈ ( bday
“ 𝐹)) |
11 | | elssuni 4403 |
. . . . . . . 8
⊢ (( bday ‘𝑛) ∈ ( bday
“ 𝐹) → ( bday ‘𝑛) ⊆ ∪ ( bday “ 𝐹)) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → ( bday ‘𝑛) ⊆ ∪ ( bday “ 𝐹)) |
13 | | bdayelon 31079 |
. . . . . . . 8
⊢ ( bday ‘𝑛) ∈ On |
14 | | imassrn 5396 |
. . . . . . . . . 10
⊢ ( bday “ 𝐹) ⊆ ran bday
|
15 | | bdayrn 31076 |
. . . . . . . . . 10
⊢ ran bday = On |
16 | 14, 15 | sseqtri 3600 |
. . . . . . . . 9
⊢ ( bday “ 𝐹) ⊆ On |
17 | | ssorduni 6877 |
. . . . . . . . 9
⊢ (( bday “ 𝐹) ⊆ On → Ord ∪ ( bday “ 𝐹)) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
⊢ Ord ∪ ( bday “ 𝐹) |
19 | | ordsssuc 5729 |
. . . . . . . 8
⊢ ((( bday ‘𝑛) ∈ On ∧ Ord ∪ ( bday “ 𝐹)) → (( bday ‘𝑛) ⊆ ∪ ( bday “ 𝐹) ↔ ( bday
‘𝑛) ∈ suc
∪ ( bday “ 𝐹))) |
20 | 13, 18, 19 | mp2an 704 |
. . . . . . 7
⊢ (( bday ‘𝑛) ⊆ ∪ ( bday “ 𝐹) ↔ ( bday
‘𝑛) ∈ suc
∪ ( bday “ 𝐹)) |
21 | 12, 20 | sylib 207 |
. . . . . 6
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → ( bday ‘𝑛) ∈ suc ∪
( bday “ 𝐹)) |
22 | | nobndlem2.1 |
. . . . . . . 8
⊢ 𝑋 ∈ {1𝑜,
2𝑜} |
23 | 22 | nosgnn0i 31056 |
. . . . . . 7
⊢ ∅
≠ 𝑋 |
24 | | fvnobday 31081 |
. . . . . . . . 9
⊢ (𝑛 ∈
No → (𝑛‘( bday
‘𝑛)) =
∅) |
25 | 3, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → (𝑛‘(
bday ‘𝑛)) =
∅) |
26 | 25 | neeq1d 2841 |
. . . . . . 7
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → ((𝑛‘(
bday ‘𝑛)) ≠
𝑋 ↔ ∅ ≠ 𝑋)) |
27 | 23, 26 | mpbiri 247 |
. . . . . 6
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → (𝑛‘(
bday ‘𝑛)) ≠
𝑋) |
28 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑏 = ( bday
‘𝑛) →
(𝑛‘𝑏) = (𝑛‘( bday
‘𝑛))) |
29 | 28 | neeq1d 2841 |
. . . . . . 7
⊢ (𝑏 = ( bday
‘𝑛) →
((𝑛‘𝑏) ≠ 𝑋 ↔ (𝑛‘( bday
‘𝑛)) ≠
𝑋)) |
30 | 29 | rspcev 3282 |
. . . . . 6
⊢ ((( bday ‘𝑛) ∈ suc ∪
( bday “ 𝐹) ∧ (𝑛‘( bday
‘𝑛)) ≠
𝑋) → ∃𝑏 ∈ suc ∪ ( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑋) |
31 | 21, 27, 30 | syl2anc 691 |
. . . . 5
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → ∃𝑏 ∈ suc ∪ ( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑋) |
32 | 31 | ralrimiva 2949 |
. . . 4
⊢ (𝐹 ⊆
No → ∀𝑛
∈ 𝐹 ∃𝑏 ∈ suc ∪ ( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑋) |
33 | | rexeq 3116 |
. . . . . 6
⊢ (𝑎 = suc ∪ ( bday “ 𝐹) → (∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋 ↔ ∃𝑏 ∈ suc ∪
( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑋)) |
34 | 33 | ralbidv 2969 |
. . . . 5
⊢ (𝑎 = suc ∪ ( bday “ 𝐹) → (∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋 ↔ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ suc ∪
( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑋)) |
35 | 34 | rspcev 3282 |
. . . 4
⊢ ((suc
∪ ( bday “ 𝐹) ∈ On ∧ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ suc ∪
( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑋) → ∃𝑎 ∈ On ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋) |
36 | 2, 32, 35 | syl2anr 494 |
. . 3
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
𝐴) → ∃𝑎 ∈ On ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋) |
37 | | onintrab2 6894 |
. . 3
⊢
(∃𝑎 ∈ On
∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋 ↔ ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋} ∈ On) |
38 | 36, 37 | sylib 207 |
. 2
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
𝐴) → ∩ {𝑎
∈ On ∣ ∀𝑛
∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑋} ∈ On) |
39 | 1, 38 | syl5eqel 2692 |
1
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
𝐴) → 𝐶 ∈ On) |