Step | Hyp | Ref
| Expression |
1 | | mapfien2.z |
. . 3
⊢ (𝜑 → 0 ∈ 𝐵) |
2 | | mapfien2.w |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝐷) |
3 | | mapfien2.bd |
. . 3
⊢ (𝜑 → 𝐵 ≈ 𝐷) |
4 | | enfixsn 8868 |
. . 3
⊢ (( 0 ∈ 𝐵 ∧ 𝑊 ∈ 𝐷 ∧ 𝐵 ≈ 𝐷) → ∃𝑦(𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) |
5 | 1, 2, 3, 4 | syl3anc 1370 |
. 2
⊢ (𝜑 → ∃𝑦(𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) |
6 | | mapfien2.ac |
. . . . 5
⊢ (𝜑 → 𝐴 ≈ 𝐶) |
7 | | bren 8743 |
. . . . 5
⊢ (𝐴 ≈ 𝐶 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝐶) |
8 | 6, 7 | sylib 217 |
. . . 4
⊢ (𝜑 → ∃𝑧 𝑧:𝐴–1-1-onto→𝐶) |
9 | | mapfien2.s |
. . . . . . . . . 10
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 0 } |
10 | | eqid 2738 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} |
11 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑦‘ 0 ) = (𝑦‘ 0 ) |
12 | | f1ocnv 6728 |
. . . . . . . . . . 11
⊢ (𝑧:𝐴–1-1-onto→𝐶 → ◡𝑧:𝐶–1-1-onto→𝐴) |
13 | 12 | 3ad2ant2 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → ◡𝑧:𝐶–1-1-onto→𝐴) |
14 | | simp3 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝑦:𝐵–1-1-onto→𝐷) |
15 | 6 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐴 ≈ 𝐶) |
16 | | relen 8738 |
. . . . . . . . . . . 12
⊢ Rel
≈ |
17 | 16 | brrelex1i 5643 |
. . . . . . . . . . 11
⊢ (𝐴 ≈ 𝐶 → 𝐴 ∈ V) |
18 | 15, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐴 ∈ V) |
19 | 3 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐵 ≈ 𝐷) |
20 | 16 | brrelex1i 5643 |
. . . . . . . . . . 11
⊢ (𝐵 ≈ 𝐷 → 𝐵 ∈ V) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐵 ∈ V) |
22 | 16 | brrelex2i 5644 |
. . . . . . . . . . 11
⊢ (𝐴 ≈ 𝐶 → 𝐶 ∈ V) |
23 | 15, 22 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐶 ∈ V) |
24 | 16 | brrelex2i 5644 |
. . . . . . . . . . 11
⊢ (𝐵 ≈ 𝐷 → 𝐷 ∈ V) |
25 | 19, 24 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐷 ∈ V) |
26 | 1 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 0 ∈ 𝐵) |
27 | 9, 10, 11, 13, 14, 18, 21, 23, 25, 26 | mapfien 9167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑤 ∈ 𝑆 ↦ (𝑦 ∘ (𝑤 ∘ ◡𝑧))):𝑆–1-1-onto→{𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )}) |
28 | | ovex 7308 |
. . . . . . . . . . 11
⊢ (𝐵 ↑m 𝐴) ∈ V |
29 | 9, 28 | rabex2 5258 |
. . . . . . . . . 10
⊢ 𝑆 ∈ V |
30 | 29 | f1oen 8761 |
. . . . . . . . 9
⊢ ((𝑤 ∈ 𝑆 ↦ (𝑦 ∘ (𝑤 ∘ ◡𝑧))):𝑆–1-1-onto→{𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} → 𝑆 ≈ {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )}) |
31 | 27, 30 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝑆 ≈ {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )}) |
32 | 31 | 3adant3r 1180 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ (𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) → 𝑆 ≈ {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )}) |
33 | | breq2 5078 |
. . . . . . . . . . 11
⊢ ((𝑦‘ 0 ) = 𝑊 → (𝑥 finSupp (𝑦‘ 0 ) ↔ 𝑥 finSupp 𝑊)) |
34 | 33 | rabbidv 3414 |
. . . . . . . . . 10
⊢ ((𝑦‘ 0 ) = 𝑊 → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}) |
35 | | mapfien2.t |
. . . . . . . . . 10
⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} |
36 | 34, 35 | eqtr4di 2796 |
. . . . . . . . 9
⊢ ((𝑦‘ 0 ) = 𝑊 → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = 𝑇) |
37 | 36 | adantl 482 |
. . . . . . . 8
⊢ ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = 𝑇) |
38 | 37 | 3ad2ant3 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ (𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = 𝑇) |
39 | 32, 38 | breqtrd 5100 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ (𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) → 𝑆 ≈ 𝑇) |
40 | 39 | 3exp 1118 |
. . . . 5
⊢ (𝜑 → (𝑧:𝐴–1-1-onto→𝐶 → ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇))) |
41 | 40 | exlimdv 1936 |
. . . 4
⊢ (𝜑 → (∃𝑧 𝑧:𝐴–1-1-onto→𝐶 → ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇))) |
42 | 8, 41 | mpd 15 |
. . 3
⊢ (𝜑 → ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇)) |
43 | 42 | exlimdv 1936 |
. 2
⊢ (𝜑 → (∃𝑦(𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇)) |
44 | 5, 43 | mpd 15 |
1
⊢ (𝜑 → 𝑆 ≈ 𝑇) |