| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mapfien2.z | . . 3
⊢ (𝜑 → 0 ∈ 𝐵) | 
| 2 |  | mapfien2.w | . . 3
⊢ (𝜑 → 𝑊 ∈ 𝐷) | 
| 3 |  | mapfien2.bd | . . 3
⊢ (𝜑 → 𝐵 ≈ 𝐷) | 
| 4 |  | enfixsn 9122 | . . 3
⊢ (( 0 ∈ 𝐵 ∧ 𝑊 ∈ 𝐷 ∧ 𝐵 ≈ 𝐷) → ∃𝑦(𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) | 
| 5 | 1, 2, 3, 4 | syl3anc 1372 | . 2
⊢ (𝜑 → ∃𝑦(𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) | 
| 6 |  | mapfien2.ac | . . . . 5
⊢ (𝜑 → 𝐴 ≈ 𝐶) | 
| 7 |  | bren 8996 | . . . . 5
⊢ (𝐴 ≈ 𝐶 ↔ ∃𝑧 𝑧:𝐴–1-1-onto→𝐶) | 
| 8 | 6, 7 | sylib 218 | . . . 4
⊢ (𝜑 → ∃𝑧 𝑧:𝐴–1-1-onto→𝐶) | 
| 9 |  | mapfien2.s | . . . . . . . . . 10
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 0 } | 
| 10 |  | eqid 2736 | . . . . . . . . . 10
⊢ {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} | 
| 11 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑦‘ 0 ) = (𝑦‘ 0 ) | 
| 12 |  | f1ocnv 6859 | . . . . . . . . . . 11
⊢ (𝑧:𝐴–1-1-onto→𝐶 → ◡𝑧:𝐶–1-1-onto→𝐴) | 
| 13 | 12 | 3ad2ant2 1134 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → ◡𝑧:𝐶–1-1-onto→𝐴) | 
| 14 |  | simp3 1138 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝑦:𝐵–1-1-onto→𝐷) | 
| 15 | 6 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐴 ≈ 𝐶) | 
| 16 |  | relen 8991 | . . . . . . . . . . . 12
⊢ Rel
≈ | 
| 17 | 16 | brrelex1i 5740 | . . . . . . . . . . 11
⊢ (𝐴 ≈ 𝐶 → 𝐴 ∈ V) | 
| 18 | 15, 17 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐴 ∈ V) | 
| 19 | 3 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐵 ≈ 𝐷) | 
| 20 | 16 | brrelex1i 5740 | . . . . . . . . . . 11
⊢ (𝐵 ≈ 𝐷 → 𝐵 ∈ V) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐵 ∈ V) | 
| 22 | 16 | brrelex2i 5741 | . . . . . . . . . . 11
⊢ (𝐴 ≈ 𝐶 → 𝐶 ∈ V) | 
| 23 | 15, 22 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐶 ∈ V) | 
| 24 | 16 | brrelex2i 5741 | . . . . . . . . . . 11
⊢ (𝐵 ≈ 𝐷 → 𝐷 ∈ V) | 
| 25 | 19, 24 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 𝐷 ∈ V) | 
| 26 | 1 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → 0 ∈ 𝐵) | 
| 27 | 9, 10, 11, 13, 14, 18, 21, 23, 25, 26 | mapfien 9449 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ 𝑦:𝐵–1-1-onto→𝐷) → (𝑤 ∈ 𝑆 ↦ (𝑦 ∘ (𝑤 ∘ ◡𝑧))):𝑆–1-1-onto→{𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )}) | 
| 28 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝐵 ↑m 𝐴) ∈ V | 
| 29 | 9, 28 | rabex2 5340 | . . . . . . . . . 10
⊢ 𝑆 ∈ V | 
| 30 | 29 | f1oen 9014 | . . . . . . . . 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 1181 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ (𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) → 𝑆 ≈ {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )}) | 
| 33 |  | breq2 5146 | . . . . . . . . . . 11
⊢ ((𝑦‘ 0 ) = 𝑊 → (𝑥 finSupp (𝑦‘ 0 ) ↔ 𝑥 finSupp 𝑊)) | 
| 34 | 33 | rabbidv 3443 | . . . . . . . . . 10
⊢ ((𝑦‘ 0 ) = 𝑊 → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊}) | 
| 35 |  | mapfien2.t | . . . . . . . . . 10
⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} | 
| 36 | 34, 35 | eqtr4di 2794 | . . . . . . . . 9
⊢ ((𝑦‘ 0 ) = 𝑊 → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = 𝑇) | 
| 37 | 36 | adantl 481 | . . . . . . . 8
⊢ ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = 𝑇) | 
| 38 | 37 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ (𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) → {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp (𝑦‘ 0 )} = 𝑇) | 
| 39 | 32, 38 | breqtrd 5168 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧:𝐴–1-1-onto→𝐶 ∧ (𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊)) → 𝑆 ≈ 𝑇) | 
| 40 | 39 | 3exp 1119 | . . . . 5
⊢ (𝜑 → (𝑧:𝐴–1-1-onto→𝐶 → ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇))) | 
| 41 | 40 | exlimdv 1932 | . . . 4
⊢ (𝜑 → (∃𝑧 𝑧:𝐴–1-1-onto→𝐶 → ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇))) | 
| 42 | 8, 41 | mpd 15 | . . 3
⊢ (𝜑 → ((𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇)) | 
| 43 | 42 | exlimdv 1932 | . 2
⊢ (𝜑 → (∃𝑦(𝑦:𝐵–1-1-onto→𝐷 ∧ (𝑦‘ 0 ) = 𝑊) → 𝑆 ≈ 𝑇)) | 
| 44 | 5, 43 | mpd 15 | 1
⊢ (𝜑 → 𝑆 ≈ 𝑇) |