Proof of Theorem nobndlem5
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3650 |
. . . 4
⊢ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ⊆ On |
2 | | nobndlem4.1 |
. . . . . . . 8
⊢ 𝑋 ∈ {1𝑜,
2𝑜} |
3 | 2 | nosgnn0i 31056 |
. . . . . . 7
⊢ ∅
≠ 𝑋 |
4 | | fvnobday 31081 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝐴‘( bday
‘𝐴)) =
∅) |
5 | 4 | neeq1d 2841 |
. . . . . . 7
⊢ (𝐴 ∈
No → ((𝐴‘( bday
‘𝐴)) ≠
𝑋 ↔ ∅ ≠ 𝑋)) |
6 | 3, 5 | mpbiri 247 |
. . . . . 6
⊢ (𝐴 ∈
No → (𝐴‘( bday
‘𝐴)) ≠
𝑋) |
7 | | bdayelon 31079 |
. . . . . . 7
⊢ ( bday ‘𝐴) ∈ On |
8 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = ( bday
‘𝐴) →
(𝐴‘𝑥) = (𝐴‘( bday
‘𝐴))) |
9 | 8 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑥 = ( bday
‘𝐴) →
((𝐴‘𝑥) ≠ 𝑋 ↔ (𝐴‘( bday
‘𝐴)) ≠
𝑋)) |
10 | 9 | elrab3 3332 |
. . . . . . 7
⊢ (( bday ‘𝐴) ∈ On → ((
bday ‘𝐴)
∈ {𝑥 ∈ On ∣
(𝐴‘𝑥) ≠ 𝑋} ↔ (𝐴‘( bday
‘𝐴)) ≠
𝑋)) |
11 | 7, 10 | ax-mp 5 |
. . . . . 6
⊢ (( bday ‘𝐴) ∈ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ↔ (𝐴‘( bday
‘𝐴)) ≠
𝑋) |
12 | 6, 11 | sylibr 223 |
. . . . 5
⊢ (𝐴 ∈
No → ( bday ‘𝐴) ∈ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) |
13 | | ne0i 3880 |
. . . . 5
⊢ (( bday ‘𝐴) ∈ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} → {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ≠ ∅) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝐴 ∈
No → {𝑥 ∈
On ∣ (𝐴‘𝑥) ≠ 𝑋} ≠ ∅) |
15 | | onint 6887 |
. . . 4
⊢ (({𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ⊆ On ∧ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ≠ ∅) → ∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ∈ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) |
16 | 1, 14, 15 | sylancr 694 |
. . 3
⊢ (𝐴 ∈
No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ∈ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) |
17 | | nfrab1 3099 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} |
18 | 17 | nfint 4421 |
. . . 4
⊢
Ⅎ𝑥∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} |
19 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑥On |
20 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥𝐴 |
21 | 20, 18 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑥(𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) |
22 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑥𝑋 |
23 | 21, 22 | nfne 2882 |
. . . 4
⊢
Ⅎ𝑥(𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) ≠ 𝑋 |
24 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} → (𝐴‘𝑥) = (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋})) |
25 | 24 | neeq1d 2841 |
. . . 4
⊢ (𝑥 = ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} → ((𝐴‘𝑥) ≠ 𝑋 ↔ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) ≠ 𝑋)) |
26 | 18, 19, 23, 25 | elrabf 3329 |
. . 3
⊢ (∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ∈ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ↔ (∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ∈ On ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) ≠ 𝑋)) |
27 | 16, 26 | sylib 207 |
. 2
⊢ (𝐴 ∈
No → (∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋} ∈ On ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) ≠ 𝑋)) |
28 | 27 | simprd 478 |
1
⊢ (𝐴 ∈
No → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ 𝑋}) ≠ 𝑋) |