Step | Hyp | Ref
| Expression |
1 | | fidcenumlemrk.k |
. 2
⊢ (𝜑 → 𝐾 ∈ ω) |
2 | | fidcenumlemrk.kn |
. . 3
⊢ (𝜑 → 𝐾 ⊆ 𝑁) |
3 | 2 | ancli 321 |
. 2
⊢ (𝜑 → (𝜑 ∧ 𝐾 ⊆ 𝑁)) |
4 | | sseq1 3170 |
. . . . 5
⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝑁 ↔ ∅ ⊆ 𝑁)) |
5 | 4 | anbi2d 461 |
. . . 4
⊢ (𝑤 = ∅ → ((𝜑 ∧ 𝑤 ⊆ 𝑁) ↔ (𝜑 ∧ ∅ ⊆ 𝑁))) |
6 | | imaeq2 4949 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝐹 “ 𝑤) = (𝐹 “ ∅)) |
7 | 6 | eleq2d 2240 |
. . . . 5
⊢ (𝑤 = ∅ → (𝑋 ∈ (𝐹 “ 𝑤) ↔ 𝑋 ∈ (𝐹 “ ∅))) |
8 | 7 | notbid 662 |
. . . . 5
⊢ (𝑤 = ∅ → (¬ 𝑋 ∈ (𝐹 “ 𝑤) ↔ ¬ 𝑋 ∈ (𝐹 “ ∅))) |
9 | 7, 8 | orbi12d 788 |
. . . 4
⊢ (𝑤 = ∅ → ((𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤)) ↔ (𝑋 ∈ (𝐹 “ ∅) ∨ ¬ 𝑋 ∈ (𝐹 “ ∅)))) |
10 | 5, 9 | imbi12d 233 |
. . 3
⊢ (𝑤 = ∅ → (((𝜑 ∧ 𝑤 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤))) ↔ ((𝜑 ∧ ∅ ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ ∅) ∨ ¬ 𝑋 ∈ (𝐹 “ ∅))))) |
11 | | sseq1 3170 |
. . . . 5
⊢ (𝑤 = 𝑗 → (𝑤 ⊆ 𝑁 ↔ 𝑗 ⊆ 𝑁)) |
12 | 11 | anbi2d 461 |
. . . 4
⊢ (𝑤 = 𝑗 → ((𝜑 ∧ 𝑤 ⊆ 𝑁) ↔ (𝜑 ∧ 𝑗 ⊆ 𝑁))) |
13 | | imaeq2 4949 |
. . . . . 6
⊢ (𝑤 = 𝑗 → (𝐹 “ 𝑤) = (𝐹 “ 𝑗)) |
14 | 13 | eleq2d 2240 |
. . . . 5
⊢ (𝑤 = 𝑗 → (𝑋 ∈ (𝐹 “ 𝑤) ↔ 𝑋 ∈ (𝐹 “ 𝑗))) |
15 | 14 | notbid 662 |
. . . . 5
⊢ (𝑤 = 𝑗 → (¬ 𝑋 ∈ (𝐹 “ 𝑤) ↔ ¬ 𝑋 ∈ (𝐹 “ 𝑗))) |
16 | 14, 15 | orbi12d 788 |
. . . 4
⊢ (𝑤 = 𝑗 → ((𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤)) ↔ (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) |
17 | 12, 16 | imbi12d 233 |
. . 3
⊢ (𝑤 = 𝑗 → (((𝜑 ∧ 𝑤 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤))) ↔ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗))))) |
18 | | sseq1 3170 |
. . . . 5
⊢ (𝑤 = suc 𝑗 → (𝑤 ⊆ 𝑁 ↔ suc 𝑗 ⊆ 𝑁)) |
19 | 18 | anbi2d 461 |
. . . 4
⊢ (𝑤 = suc 𝑗 → ((𝜑 ∧ 𝑤 ⊆ 𝑁) ↔ (𝜑 ∧ suc 𝑗 ⊆ 𝑁))) |
20 | | imaeq2 4949 |
. . . . . 6
⊢ (𝑤 = suc 𝑗 → (𝐹 “ 𝑤) = (𝐹 “ suc 𝑗)) |
21 | 20 | eleq2d 2240 |
. . . . 5
⊢ (𝑤 = suc 𝑗 → (𝑋 ∈ (𝐹 “ 𝑤) ↔ 𝑋 ∈ (𝐹 “ suc 𝑗))) |
22 | 21 | notbid 662 |
. . . . 5
⊢ (𝑤 = suc 𝑗 → (¬ 𝑋 ∈ (𝐹 “ 𝑤) ↔ ¬ 𝑋 ∈ (𝐹 “ suc 𝑗))) |
23 | 21, 22 | orbi12d 788 |
. . . 4
⊢ (𝑤 = suc 𝑗 → ((𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤)) ↔ (𝑋 ∈ (𝐹 “ suc 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝑗)))) |
24 | 19, 23 | imbi12d 233 |
. . 3
⊢ (𝑤 = suc 𝑗 → (((𝜑 ∧ 𝑤 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤))) ↔ ((𝜑 ∧ suc 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ suc 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝑗))))) |
25 | | sseq1 3170 |
. . . . 5
⊢ (𝑤 = 𝐾 → (𝑤 ⊆ 𝑁 ↔ 𝐾 ⊆ 𝑁)) |
26 | 25 | anbi2d 461 |
. . . 4
⊢ (𝑤 = 𝐾 → ((𝜑 ∧ 𝑤 ⊆ 𝑁) ↔ (𝜑 ∧ 𝐾 ⊆ 𝑁))) |
27 | | imaeq2 4949 |
. . . . . 6
⊢ (𝑤 = 𝐾 → (𝐹 “ 𝑤) = (𝐹 “ 𝐾)) |
28 | 27 | eleq2d 2240 |
. . . . 5
⊢ (𝑤 = 𝐾 → (𝑋 ∈ (𝐹 “ 𝑤) ↔ 𝑋 ∈ (𝐹 “ 𝐾))) |
29 | 28 | notbid 662 |
. . . . 5
⊢ (𝑤 = 𝐾 → (¬ 𝑋 ∈ (𝐹 “ 𝑤) ↔ ¬ 𝑋 ∈ (𝐹 “ 𝐾))) |
30 | 28, 29 | orbi12d 788 |
. . . 4
⊢ (𝑤 = 𝐾 → ((𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤)) ↔ (𝑋 ∈ (𝐹 “ 𝐾) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐾)))) |
31 | 26, 30 | imbi12d 233 |
. . 3
⊢ (𝑤 = 𝐾 → (((𝜑 ∧ 𝑤 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑤) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑤))) ↔ ((𝜑 ∧ 𝐾 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝐾) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐾))))) |
32 | | noel 3418 |
. . . . . 6
⊢ ¬
𝑋 ∈
∅ |
33 | | ima0 4970 |
. . . . . . 7
⊢ (𝐹 “ ∅) =
∅ |
34 | 33 | eleq2i 2237 |
. . . . . 6
⊢ (𝑋 ∈ (𝐹 “ ∅) ↔ 𝑋 ∈ ∅) |
35 | 32, 34 | mtbir 666 |
. . . . 5
⊢ ¬
𝑋 ∈ (𝐹 “ ∅) |
36 | 35 | a1i 9 |
. . . 4
⊢ ((𝜑 ∧ ∅ ⊆ 𝑁) → ¬ 𝑋 ∈ (𝐹 “ ∅)) |
37 | 36 | olcd 729 |
. . 3
⊢ ((𝜑 ∧ ∅ ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ ∅) ∨ ¬ 𝑋 ∈ (𝐹 “ ∅))) |
38 | | fidcenumlemr.dc |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
39 | 38 | ad2antrl 487 |
. . . . 5
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
40 | | fidcenumlemr.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) |
41 | 40 | ad2antrl 487 |
. . . . 5
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → 𝐹:𝑁–onto→𝐴) |
42 | | simpll 524 |
. . . . 5
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → 𝑗 ∈ ω) |
43 | | simprr 527 |
. . . . 5
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → suc 𝑗 ⊆ 𝑁) |
44 | | simprl 526 |
. . . . . 6
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → 𝜑) |
45 | | sssucid 4400 |
. . . . . . 7
⊢ 𝑗 ⊆ suc 𝑗 |
46 | 45, 43 | sstrid 3158 |
. . . . . 6
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → 𝑗 ⊆ 𝑁) |
47 | | simplr 525 |
. . . . . 6
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) |
48 | 44, 46, 47 | mp2and 431 |
. . . . 5
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗))) |
49 | | fidcenumlemrk.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
50 | 49 | ad2antrl 487 |
. . . . 5
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → 𝑋 ∈ 𝐴) |
51 | 39, 41, 42, 43, 48, 50 | fidcenumlemrks 6930 |
. . . 4
⊢ (((𝑗 ∈ ω ∧ ((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗)))) ∧ (𝜑 ∧ suc 𝑗 ⊆ 𝑁)) → (𝑋 ∈ (𝐹 “ suc 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝑗))) |
52 | 51 | exp31 362 |
. . 3
⊢ (𝑗 ∈ ω → (((𝜑 ∧ 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝑗))) → ((𝜑 ∧ suc 𝑗 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ suc 𝑗) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝑗))))) |
53 | 10, 17, 24, 31, 37, 52 | finds 4584 |
. 2
⊢ (𝐾 ∈ ω → ((𝜑 ∧ 𝐾 ⊆ 𝑁) → (𝑋 ∈ (𝐹 “ 𝐾) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐾)))) |
54 | 1, 3, 53 | sylc 62 |
1
⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐾) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐾))) |