Proof of Theorem cantnflem1c
Step | Hyp | Ref
| Expression |
1 | | cantnfs.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ On) |
2 | 1 | ad3antrrr 762 |
. 2
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝐵 ∈ On) |
3 | | simplr 788 |
. 2
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ 𝐵) |
4 | | oemapval.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
5 | | cantnfs.s |
. . . . . . 7
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
6 | | cantnfs.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ On) |
7 | 5, 6, 1 | cantnfs 8446 |
. . . . . 6
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
8 | 4, 7 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
9 | 8 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
10 | | ffn 5958 |
. . . 4
⊢ (𝐺:𝐵⟶𝐴 → 𝐺 Fn 𝐵) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 Fn 𝐵) |
12 | 11 | ad3antrrr 762 |
. 2
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝐺 Fn 𝐵) |
13 | | oemapval.t |
. . . . . . 7
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
14 | | oemapval.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
15 | | oemapvali.r |
. . . . . . 7
⊢ (𝜑 → 𝐹𝑇𝐺) |
16 | | oemapvali.x |
. . . . . . 7
⊢ 𝑋 = ∪
{𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} |
17 | 5, 6, 1, 13, 14, 4, 15, 16 | oemapvali 8464 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
18 | 17 | simp3d 1068 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))) |
19 | 18 | ad3antrrr 762 |
. . . 4
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))) |
20 | | cantnflem1.o |
. . . . . . 7
⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) |
21 | 5, 6, 1, 13, 14, 4, 15, 16, 20 | cantnflem1b 8466 |
. . . . . 6
⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ⊆ (𝑂‘𝑢)) |
22 | 21 | ad2antrr 758 |
. . . . 5
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑋 ⊆ (𝑂‘𝑢)) |
23 | | simprr 792 |
. . . . 5
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ 𝑥) |
24 | 17 | simp1d 1066 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
25 | | onelon 5665 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On) |
26 | 1, 24, 25 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ On) |
27 | 26 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑋 ∈ On) |
28 | | onss 6882 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
29 | 1, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ On) |
30 | 29 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
31 | 30 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ On) |
33 | | ontr2 5689 |
. . . . . 6
⊢ ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂‘𝑢) ∧ (𝑂‘𝑢) ∈ 𝑥) → 𝑋 ∈ 𝑥)) |
34 | 27, 32, 33 | syl2anc 691 |
. . . . 5
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂‘𝑢) ∧ (𝑂‘𝑢) ∈ 𝑥) → 𝑋 ∈ 𝑥)) |
35 | 22, 23, 34 | mp2and 711 |
. . . 4
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑋 ∈ 𝑥) |
36 | | eleq2 2677 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥)) |
37 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
38 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (𝐺‘𝑤) = (𝐺‘𝑥)) |
39 | 37, 38 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑤 = 𝑥 → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘𝑥) = (𝐺‘𝑥))) |
40 | 36, 39 | imbi12d 333 |
. . . . 5
⊢ (𝑤 = 𝑥 → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥)))) |
41 | 40 | rspcv 3278 |
. . . 4
⊢ (𝑥 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥)))) |
42 | 3, 19, 35, 41 | syl3c 64 |
. . 3
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
43 | | simprl 790 |
. . 3
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝐹‘𝑥) ≠ ∅) |
44 | 42, 43 | eqnetrrd 2850 |
. 2
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝐺‘𝑥) ≠ ∅) |
45 | | fvn0elsupp 7198 |
. 2
⊢ (((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) ∧ (𝐺 Fn 𝐵 ∧ (𝐺‘𝑥) ≠ ∅)) → 𝑥 ∈ (𝐺 supp ∅)) |
46 | 2, 3, 12, 44, 45 | syl22anc 1319 |
1
⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅)) |