Proof of Theorem oef1o
Step | Hyp | Ref
| Expression |
1 | | eqid 2818 |
. . . . 5
⊢ dom
(𝐶 CNF 𝐷) = dom (𝐶 CNF 𝐷) |
2 | | oef1o.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ On) |
3 | | oef1o.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ On) |
4 | 1, 2, 3 | cantnff1o 9147 |
. . . 4
⊢ (𝜑 → (𝐶 CNF 𝐷):dom (𝐶 CNF 𝐷)–1-1-onto→(𝐶 ↑o 𝐷)) |
5 | | eqid 2818 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} |
6 | | eqid 2818 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} = {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} |
7 | | eqid 2818 |
. . . . . . . 8
⊢ (𝐹‘∅) = (𝐹‘∅) |
8 | | oef1o.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) |
9 | | f1ocnv 6620 |
. . . . . . . . 9
⊢ (𝐺:𝐵–1-1-onto→𝐷 → ◡𝐺:𝐷–1-1-onto→𝐵) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ◡𝐺:𝐷–1-1-onto→𝐵) |
11 | | oef1o.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶) |
12 | | oef1o.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ On) |
13 | 12 | elexd 3512 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ V) |
14 | | oef1o.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (On ∖
1o)) |
15 | 14 | elexd 3512 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ V) |
16 | 3 | elexd 3512 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ V) |
17 | 2 | elexd 3512 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ V) |
18 | | ondif1 8115 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (On ∖
1o) ↔ (𝐴
∈ On ∧ ∅ ∈ 𝐴)) |
19 | 18 | simprbi 497 |
. . . . . . . . 9
⊢ (𝐴 ∈ (On ∖
1o) → ∅ ∈ 𝐴) |
20 | 14, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈ 𝐴) |
21 | 5, 6, 7, 10, 11, 13, 15, 16, 17, 20 | mapfien 8859 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))):{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
22 | | oef1o.k |
. . . . . . . 8
⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))) |
23 | | f1oeq1 6597 |
. . . . . . . 8
⊢ (𝐾 = (𝑦 ∈ {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))) → (𝐾:{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} ↔ (𝑦 ∈ {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))):{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)})) |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
⊢ (𝐾:{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} ↔ (𝑦 ∈ {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡𝐺))):{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
25 | 21, 24 | sylibr 235 |
. . . . . 6
⊢ (𝜑 → 𝐾:{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
26 | | eqid 2818 |
. . . . . . . . 9
⊢ {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp ∅} = {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp ∅} |
27 | 26, 2, 3 | cantnfdm 9115 |
. . . . . . . 8
⊢ (𝜑 → dom (𝐶 CNF 𝐷) = {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp ∅}) |
28 | | oef1o.z |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘∅) = ∅) |
29 | 28 | breq2d 5069 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 finSupp (𝐹‘∅) ↔ 𝑥 finSupp ∅)) |
30 | 29 | rabbidv 3478 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)} = {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp ∅}) |
31 | 27, 30 | eqtr4d 2856 |
. . . . . . 7
⊢ (𝜑 → dom (𝐶 CNF 𝐷) = {𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)}) |
32 | 31 | f1oeq3d 6605 |
. . . . . 6
⊢ (𝜑 → (𝐾:{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷) ↔ 𝐾:{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→{𝑥 ∈ (𝐶 ↑m 𝐷) ∣ 𝑥 finSupp (𝐹‘∅)})) |
33 | 25, 32 | mpbird 258 |
. . . . 5
⊢ (𝜑 → 𝐾:{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷)) |
34 | 14 | eldifad 3945 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ On) |
35 | 5, 34, 12 | cantnfdm 9115 |
. . . . . 6
⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}) |
36 | 35 | f1oeq2d 6604 |
. . . . 5
⊢ (𝜑 → (𝐾:dom (𝐴 CNF 𝐵)–1-1-onto→dom
(𝐶 CNF 𝐷) ↔ 𝐾:{𝑥 ∈ (𝐴 ↑m 𝐵) ∣ 𝑥 finSupp ∅}–1-1-onto→dom
(𝐶 CNF 𝐷))) |
37 | 33, 36 | mpbird 258 |
. . . 4
⊢ (𝜑 → 𝐾:dom (𝐴 CNF 𝐵)–1-1-onto→dom
(𝐶 CNF 𝐷)) |
38 | | f1oco 6630 |
. . . 4
⊢ (((𝐶 CNF 𝐷):dom (𝐶 CNF 𝐷)–1-1-onto→(𝐶 ↑o 𝐷) ∧ 𝐾:dom (𝐴 CNF 𝐵)–1-1-onto→dom
(𝐶 CNF 𝐷)) → ((𝐶 CNF 𝐷) ∘ 𝐾):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐶 ↑o 𝐷)) |
39 | 4, 37, 38 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝐶 CNF 𝐷) ∘ 𝐾):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐶 ↑o 𝐷)) |
40 | | eqid 2818 |
. . . . 5
⊢ dom
(𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵) |
41 | 40, 34, 12 | cantnff1o 9147 |
. . . 4
⊢ (𝜑 → (𝐴 CNF 𝐵):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐴 ↑o 𝐵)) |
42 | | f1ocnv 6620 |
. . . 4
⊢ ((𝐴 CNF 𝐵):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐴 ↑o 𝐵) → ◡(𝐴 CNF 𝐵):(𝐴 ↑o 𝐵)–1-1-onto→dom
(𝐴 CNF 𝐵)) |
43 | 41, 42 | syl 17 |
. . 3
⊢ (𝜑 → ◡(𝐴 CNF 𝐵):(𝐴 ↑o 𝐵)–1-1-onto→dom
(𝐴 CNF 𝐵)) |
44 | | f1oco 6630 |
. . 3
⊢ ((((𝐶 CNF 𝐷) ∘ 𝐾):dom (𝐴 CNF 𝐵)–1-1-onto→(𝐶 ↑o 𝐷) ∧ ◡(𝐴 CNF 𝐵):(𝐴 ↑o 𝐵)–1-1-onto→dom
(𝐴 CNF 𝐵)) → (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷)) |
45 | 39, 43, 44 | syl2anc 584 |
. 2
⊢ (𝜑 → (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷)) |
46 | | oef1o.h |
. . 3
⊢ 𝐻 = (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)) |
47 | | f1oeq1 6597 |
. . 3
⊢ (𝐻 = (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)) → (𝐻:(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷) ↔ (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷))) |
48 | 46, 47 | ax-mp 5 |
. 2
⊢ (𝐻:(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷) ↔ (((𝐶 CNF 𝐷) ∘ 𝐾) ∘ ◡(𝐴 CNF 𝐵)):(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷)) |
49 | 45, 48 | sylibr 235 |
1
⊢ (𝜑 → 𝐻:(𝐴 ↑o 𝐵)–1-1-onto→(𝐶 ↑o 𝐷)) |