Proof of Theorem oef1o
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢ dom
(𝐶 CNF 𝐷) = dom (𝐶 CNF 𝐷) |
2 | | oef1o.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ On) |
3 | | oef1o.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ On) |
4 | 1, 2, 3 | cantnff1o 8476 |
. . . 4
⊢ (𝜑 → (𝐶 CNF 𝐷):dom (𝐶 CNF 𝐷)–1-1-onto→(𝐶 ↑𝑜 𝐷)) |
5 | | eqid 2610 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} |
6 | | eqid 2610 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} = {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} |
7 | | eqid 2610 |
. . . . . . . 8
⊢ (𝐹‘∅) = (𝐹‘∅) |
8 | | oef1o.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) |
9 | | f1ocnv 6062 |
. . . . . . . . 9
⊢ (𝐺:𝐵–1-1-onto→𝐷 → ◡𝐺:𝐷–1-1-onto→𝐵) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐺:𝐷–1-1-onto→𝐵) |
11 | | oef1o.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶) |
12 | | ssv 3588 |
. . . . . . . . 9
⊢ On
⊆ V |
13 | | oef1o.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ On) |
14 | 12, 13 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ V) |
15 | | oef1o.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (On ∖
1𝑜)) |
16 | 15 | eldifad 3552 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ On) |
17 | 12, 16 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ V) |
18 | 12, 3 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ V) |
19 | 12, 2 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ V) |
20 | | ondif1 7468 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (On ∖
1𝑜) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) |
21 | 20 | simprbi 479 |
. . . . . . . . 9
⊢ (𝐴 ∈ (On ∖
1𝑜) → ∅ ∈ 𝐴) |
22 | 15, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈ 𝐴) |
23 | 5, 6, 7, 10, 11, 14, 17, 18, 19, 22 | mapfien 8196 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))):{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
24 | | oef1o.k |
. . . . . . . 8
⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))) |
25 | | f1oeq1 6040 |
. . . . . . . 8
⊢ (𝐾 = (𝑦 ∈ {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))) → (𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} ↔ (𝑦 ∈ {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))):{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)})) |
26 | 24, 25 | ax-mp 5 |
. . . . . . 7
⊢ (𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} ↔ (𝑦 ∈ {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))):{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
27 | 23, 26 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → 𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
28 | | eqid 2610 |
. . . . . . . . 9
⊢ {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp ∅} |
29 | 28, 2, 3 | cantnfdm 8444 |
. . . . . . . 8
⊢ (𝜑 → dom (𝐶 CNF 𝐷) = {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp ∅}) |
30 | | oef1o.z |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘∅) = ∅) |
31 | 30 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 finSupp (𝐹‘∅) ↔ 𝑥 finSupp ∅)) |
32 | 31 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} = {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp ∅}) |
33 | 29, 32 | eqtr4d 2647 |
. . . . . . 7
⊢ (𝜑 → dom (𝐶 CNF 𝐷) = {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
34 | | f1oeq3 6042 |
. . . . . . 7
⊢ (dom
(𝐶 CNF 𝐷) = {𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} → (𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷) ↔ 𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)})) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷) ↔ 𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑𝑚 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)})) |
36 | 27, 35 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷)) |
37 | 5, 16, 13 | cantnfdm 8444 |
. . . . . 6
⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}) |
38 | | f1oeq2 6041 |
. . . . . 6
⊢ (dom
(𝐴 CNF 𝐵) = {𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅} → (𝐾:dom (𝐴 CNF 𝐵)–1-1-onto→dom
(𝐶 CNF 𝐷) ↔ 𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷))) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾:dom (𝐴 CNF 𝐵)–1-1-onto→dom
(𝐶 CNF 𝐷) ↔ 𝐾:{𝑥 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷))) |
40 | 36, 39 | mpbird 246 |
. . . 4
⊢ (𝜑 → 𝐾:dom (𝐴 CNF 𝐵)–1-1-onto→dom
(𝐶 CNF 𝐷)) |
41 | | f1oco 6072 |
. . . 4
⊢ (((𝐶 CNF 𝐷):dom (𝐶 CNF 𝐷)–1-1-onto→(𝐶 ↑𝑜 𝐷) ∧ 𝐾:dom (𝐴 CNF 𝐵)–1-1-onto→dom
(𝐶 CNF 𝐷)) → ((𝐶 CNF 𝐷) ∘ 𝐾):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷)) |
42 | 4, 40, 41 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝐶 CNF 𝐷) ∘ 𝐾):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷)) |
43 | | eqid 2610 |
. . . . 5
⊢ dom
(𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵) |
44 | 43, 16, 13 | cantnff1o 8476 |
. . . 4
⊢ (𝜑 → (𝐴 CNF 𝐵):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐴 ↑𝑜 𝐵)) |
45 | | f1ocnv 6062 |
. . . 4
⊢ ((𝐴 CNF 𝐵):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐴 ↑𝑜 𝐵) → ◡(𝐴 CNF 𝐵):(𝐴 ↑𝑜 𝐵)–1-1-onto→dom
(𝐴 CNF 𝐵)) |
46 | 44, 45 | syl 17 |
. . 3
⊢ (𝜑 → ◡(𝐴 CNF 𝐵):(𝐴 ↑𝑜 𝐵)–1-1-onto→dom
(𝐴 CNF 𝐵)) |
47 | | f1oco 6072 |
. . 3
⊢ ((((𝐶 CNF 𝐷) ∘ 𝐾):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷) ∧ ◡(𝐴 CNF 𝐵):(𝐴 ↑𝑜 𝐵)–1-1-onto→dom
(𝐴 CNF 𝐵)) → (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷)) |
48 | 42, 46, 47 | syl2anc 691 |
. 2
⊢ (𝜑 → (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷)) |
49 | | oef1o.h |
. . 3
⊢ 𝐻 = (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)) |
50 | | f1oeq1 6040 |
. . 3
⊢ (𝐻 = (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)) → (𝐻:(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷) ↔ (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷))) |
51 | 49, 50 | ax-mp 5 |
. 2
⊢ (𝐻:(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷) ↔ (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷)) |
52 | 48, 51 | sylibr 223 |
1
⊢ (𝜑 → 𝐻:(𝐴 ↑𝑜 𝐵)–1-1-onto→(𝐶 ↑𝑜 𝐷)) |