Proof of Theorem nobndlem8
Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐹 ∈ 𝐴 → 𝐹 ∈ V) |
2 | | nobndlem8.1 |
. . . . 5
⊢ 𝑆 ∈ {1𝑜,
2𝑜} |
3 | | nobndlem8.2 |
. . . . 5
⊢ 𝐶 = ∩
{𝑎 ∈ On ∣
∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑆} |
4 | 2, 3 | nobndlem3 31093 |
. . . 4
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
V) → ( bday ‘(𝐶 × {𝑆})) = 𝐶) |
5 | 4, 3 | syl6eq 2660 |
. . 3
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
V) → ( bday ‘(𝐶 × {𝑆})) = ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑆}) |
6 | | nobndlem1 31091 |
. . . . 5
⊢ (𝐹 ∈ V → suc ∪ ( bday “ 𝐹) ∈ On) |
7 | 6 | adantl 481 |
. . . 4
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
V) → suc ∪ ( bday
“ 𝐹) ∈
On) |
8 | | bdayfn 31078 |
. . . . . . . . . . 11
⊢ bday Fn No
|
9 | | fnfvima 6400 |
. . . . . . . . . . 11
⊢ (( bday Fn No ∧ 𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → ( bday ‘𝑛) ∈ ( bday
“ 𝐹)) |
10 | 8, 9 | mp3an1 1403 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → ( bday ‘𝑛) ∈ ( bday
“ 𝐹)) |
11 | 10 | 3adant2 1073 |
. . . . . . . . 9
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈ V
∧ 𝑛 ∈ 𝐹) → (
bday ‘𝑛)
∈ ( bday “ 𝐹)) |
12 | | elssuni 4403 |
. . . . . . . . 9
⊢ (( bday ‘𝑛) ∈ ( bday
“ 𝐹) → ( bday ‘𝑛) ⊆ ∪ ( bday “ 𝐹)) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈ V
∧ 𝑛 ∈ 𝐹) → (
bday ‘𝑛)
⊆ ∪ ( bday
“ 𝐹)) |
14 | | bdayelon 31079 |
. . . . . . . . 9
⊢ ( bday ‘𝑛) ∈ On |
15 | | sucelon 6909 |
. . . . . . . . . . 11
⊢ (∪ ( bday “ 𝐹) ∈ On ↔ suc ∪ ( bday “ 𝐹) ∈ On) |
16 | 6, 15 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝐹 ∈ V → ∪ ( bday “ 𝐹) ∈ On) |
17 | 16 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈ V
∧ 𝑛 ∈ 𝐹) → ∪ ( bday “ 𝐹) ∈ On) |
18 | | onsssuc 5730 |
. . . . . . . . 9
⊢ ((( bday ‘𝑛) ∈ On ∧ ∪ ( bday “ 𝐹) ∈ On) → (( bday ‘𝑛) ⊆ ∪ ( bday “ 𝐹) ↔ ( bday
‘𝑛) ∈ suc
∪ ( bday “ 𝐹))) |
19 | 14, 17, 18 | sylancr 694 |
. . . . . . . 8
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈ V
∧ 𝑛 ∈ 𝐹) → (( bday ‘𝑛) ⊆ ∪ ( bday “ 𝐹) ↔ ( bday
‘𝑛) ∈ suc
∪ ( bday “ 𝐹))) |
20 | 13, 19 | mpbid 221 |
. . . . . . 7
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈ V
∧ 𝑛 ∈ 𝐹) → (
bday ‘𝑛)
∈ suc ∪ ( bday
“ 𝐹)) |
21 | | ssel2 3563 |
. . . . . . . . 9
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → 𝑛 ∈
No ) |
22 | | fvnobday 31081 |
. . . . . . . . . 10
⊢ (𝑛 ∈
No → (𝑛‘( bday
‘𝑛)) =
∅) |
23 | 2 | nosgnn0i 31056 |
. . . . . . . . . . 11
⊢ ∅
≠ 𝑆 |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈
No → ∅ ≠ 𝑆) |
25 | 22, 24 | eqnetrd 2849 |
. . . . . . . . 9
⊢ (𝑛 ∈
No → (𝑛‘( bday
‘𝑛)) ≠
𝑆) |
26 | 21, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ⊆
No ∧ 𝑛 ∈
𝐹) → (𝑛‘(
bday ‘𝑛)) ≠
𝑆) |
27 | 26 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈ V
∧ 𝑛 ∈ 𝐹) → (𝑛‘( bday
‘𝑛)) ≠
𝑆) |
28 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑏 = ( bday
‘𝑛) →
(𝑛‘𝑏) = (𝑛‘( bday
‘𝑛))) |
29 | 28 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑏 = ( bday
‘𝑛) →
((𝑛‘𝑏) ≠ 𝑆 ↔ (𝑛‘( bday
‘𝑛)) ≠
𝑆)) |
30 | 29 | rspcev 3282 |
. . . . . . 7
⊢ ((( bday ‘𝑛) ∈ suc ∪
( bday “ 𝐹) ∧ (𝑛‘( bday
‘𝑛)) ≠
𝑆) → ∃𝑏 ∈ suc ∪ ( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑆) |
31 | 20, 27, 30 | syl2anc 691 |
. . . . . 6
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈ V
∧ 𝑛 ∈ 𝐹) → ∃𝑏 ∈ suc ∪ ( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑆) |
32 | 31 | 3expa 1257 |
. . . . 5
⊢ (((𝐹 ⊆
No ∧ 𝐹 ∈
V) ∧ 𝑛 ∈ 𝐹) → ∃𝑏 ∈ suc ∪ ( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑆) |
33 | 32 | ralrimiva 2949 |
. . . 4
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
V) → ∀𝑛 ∈
𝐹 ∃𝑏 ∈ suc ∪
( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑆) |
34 | | rexeq 3116 |
. . . . . 6
⊢ (𝑎 = suc ∪ ( bday “ 𝐹) → (∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑆 ↔ ∃𝑏 ∈ suc ∪
( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑆)) |
35 | 34 | ralbidv 2969 |
. . . . 5
⊢ (𝑎 = suc ∪ ( bday “ 𝐹) → (∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑆 ↔ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ suc ∪
( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑆)) |
36 | 35 | intminss 4438 |
. . . 4
⊢ ((suc
∪ ( bday “ 𝐹) ∈ On ∧ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ suc ∪
( bday “ 𝐹)(𝑛‘𝑏) ≠ 𝑆) → ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑆} ⊆ suc ∪
( bday “ 𝐹)) |
37 | 7, 33, 36 | syl2anc 691 |
. . 3
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
V) → ∩ {𝑎 ∈ On ∣ ∀𝑛 ∈ 𝐹 ∃𝑏 ∈ 𝑎 (𝑛‘𝑏) ≠ 𝑆} ⊆ suc ∪
( bday “ 𝐹)) |
38 | 5, 37 | eqsstrd 3602 |
. 2
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
V) → ( bday ‘(𝐶 × {𝑆})) ⊆ suc ∪
( bday “ 𝐹)) |
39 | 1, 38 | sylan2 490 |
1
⊢ ((𝐹 ⊆
No ∧ 𝐹 ∈
𝐴) → ( bday ‘(𝐶 × {𝑆})) ⊆ suc ∪
( bday “ 𝐹)) |