Proof of Theorem mapsncnv
| Step | Hyp | Ref
 | Expression | 
| 1 |   | elmapi 6729 | 
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → 𝑥:{𝑋}⟶𝐵) | 
| 2 |   | mapsncnv.x | 
. . . . . . . . . 10
⊢ 𝑋 ∈ V | 
| 3 | 2 | snid 3653 | 
. . . . . . . . 9
⊢ 𝑋 ∈ {𝑋} | 
| 4 |   | ffvelcdm 5695 | 
. . . . . . . . 9
⊢ ((𝑥:{𝑋}⟶𝐵 ∧ 𝑋 ∈ {𝑋}) → (𝑥‘𝑋) ∈ 𝐵) | 
| 5 | 1, 3, 4 | sylancl 413 | 
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → (𝑥‘𝑋) ∈ 𝐵) | 
| 6 |   | eqid 2196 | 
. . . . . . . . 9
⊢ {𝑋} = {𝑋} | 
| 7 |   | mapsncnv.b | 
. . . . . . . . 9
⊢ 𝐵 ∈ V | 
| 8 | 6, 7, 2 | mapsnconst 6753 | 
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → 𝑥 = ({𝑋} × {(𝑥‘𝑋)})) | 
| 9 | 5, 8 | jca 306 | 
. . . . . . 7
⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → ((𝑥‘𝑋) ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {(𝑥‘𝑋)}))) | 
| 10 |   | eleq1 2259 | 
. . . . . . . 8
⊢ (𝑦 = (𝑥‘𝑋) → (𝑦 ∈ 𝐵 ↔ (𝑥‘𝑋) ∈ 𝐵)) | 
| 11 |   | sneq 3633 | 
. . . . . . . . . 10
⊢ (𝑦 = (𝑥‘𝑋) → {𝑦} = {(𝑥‘𝑋)}) | 
| 12 | 11 | xpeq2d 4687 | 
. . . . . . . . 9
⊢ (𝑦 = (𝑥‘𝑋) → ({𝑋} × {𝑦}) = ({𝑋} × {(𝑥‘𝑋)})) | 
| 13 | 12 | eqeq2d 2208 | 
. . . . . . . 8
⊢ (𝑦 = (𝑥‘𝑋) → (𝑥 = ({𝑋} × {𝑦}) ↔ 𝑥 = ({𝑋} × {(𝑥‘𝑋)}))) | 
| 14 | 10, 13 | anbi12d 473 | 
. . . . . . 7
⊢ (𝑦 = (𝑥‘𝑋) → ((𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})) ↔ ((𝑥‘𝑋) ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {(𝑥‘𝑋)})))) | 
| 15 | 9, 14 | syl5ibrcom 157 | 
. . . . . 6
⊢ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) → (𝑦 = (𝑥‘𝑋) → (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})))) | 
| 16 | 15 | imp 124 | 
. . . . 5
⊢ ((𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)) → (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦}))) | 
| 17 |   | fconst6g 5456 | 
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → ({𝑋} × {𝑦}):{𝑋}⟶𝐵) | 
| 18 | 2 | snex 4218 | 
. . . . . . . . . 10
⊢ {𝑋} ∈ V | 
| 19 | 7, 18 | elmap 6736 | 
. . . . . . . . 9
⊢ (({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}) ↔ ({𝑋} × {𝑦}):{𝑋}⟶𝐵) | 
| 20 | 17, 19 | sylibr 134 | 
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → ({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋})) | 
| 21 |   | vex 2766 | 
. . . . . . . . . . 11
⊢ 𝑦 ∈ V | 
| 22 | 21 | fvconst2 5778 | 
. . . . . . . . . 10
⊢ (𝑋 ∈ {𝑋} → (({𝑋} × {𝑦})‘𝑋) = 𝑦) | 
| 23 | 3, 22 | mp1i 10 | 
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → (({𝑋} × {𝑦})‘𝑋) = 𝑦) | 
| 24 | 23 | eqcomd 2202 | 
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → 𝑦 = (({𝑋} × {𝑦})‘𝑋)) | 
| 25 | 20, 24 | jca 306 | 
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → (({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (({𝑋} × {𝑦})‘𝑋))) | 
| 26 |   | eleq1 2259 | 
. . . . . . . 8
⊢ (𝑥 = ({𝑋} × {𝑦}) → (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ↔ ({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}))) | 
| 27 |   | fveq1 5557 | 
. . . . . . . . 9
⊢ (𝑥 = ({𝑋} × {𝑦}) → (𝑥‘𝑋) = (({𝑋} × {𝑦})‘𝑋)) | 
| 28 | 27 | eqeq2d 2208 | 
. . . . . . . 8
⊢ (𝑥 = ({𝑋} × {𝑦}) → (𝑦 = (𝑥‘𝑋) ↔ 𝑦 = (({𝑋} × {𝑦})‘𝑋))) | 
| 29 | 26, 28 | anbi12d 473 | 
. . . . . . 7
⊢ (𝑥 = ({𝑋} × {𝑦}) → ((𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (({𝑋} × {𝑦}) ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (({𝑋} × {𝑦})‘𝑋)))) | 
| 30 | 25, 29 | syl5ibrcom 157 | 
. . . . . 6
⊢ (𝑦 ∈ 𝐵 → (𝑥 = ({𝑋} × {𝑦}) → (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)))) | 
| 31 | 30 | imp 124 | 
. . . . 5
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦})) → (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋))) | 
| 32 | 16, 31 | impbii 126 | 
. . . 4
⊢ ((𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦}))) | 
| 33 |   | mapsncnv.s | 
. . . . . . 7
⊢ 𝑆 = {𝑋} | 
| 34 | 33 | oveq2i 5933 | 
. . . . . 6
⊢ (𝐵 ↑𝑚
𝑆) = (𝐵 ↑𝑚 {𝑋}) | 
| 35 | 34 | eleq2i 2263 | 
. . . . 5
⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↔ 𝑥 ∈ (𝐵 ↑𝑚 {𝑋})) | 
| 36 | 35 | anbi1i 458 | 
. . . 4
⊢ ((𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (𝑥 ∈ (𝐵 ↑𝑚 {𝑋}) ∧ 𝑦 = (𝑥‘𝑋))) | 
| 37 | 33 | xpeq1i 4683 | 
. . . . . 6
⊢ (𝑆 × {𝑦}) = ({𝑋} × {𝑦}) | 
| 38 | 37 | eqeq2i 2207 | 
. . . . 5
⊢ (𝑥 = (𝑆 × {𝑦}) ↔ 𝑥 = ({𝑋} × {𝑦})) | 
| 39 | 38 | anbi2i 457 | 
. . . 4
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦})) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = ({𝑋} × {𝑦}))) | 
| 40 | 32, 36, 39 | 3bitr4i 212 | 
. . 3
⊢ ((𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦}))) | 
| 41 | 40 | opabbii 4100 | 
. 2
⊢
{〈𝑦, 𝑥〉 ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} = {〈𝑦, 𝑥〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦}))} | 
| 42 |   | mapsncnv.f | 
. . . . 5
⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) | 
| 43 |   | df-mpt 4096 | 
. . . . 5
⊢ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} | 
| 44 | 42, 43 | eqtri 2217 | 
. . . 4
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} | 
| 45 | 44 | cnveqi 4841 | 
. . 3
⊢ ◡𝐹 = ◡{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} | 
| 46 |   | cnvopab 5071 | 
. . 3
⊢ ◡{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} = {〈𝑦, 𝑥〉 ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} | 
| 47 | 45, 46 | eqtri 2217 | 
. 2
⊢ ◡𝐹 = {〈𝑦, 𝑥〉 ∣ (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑦 = (𝑥‘𝑋))} | 
| 48 |   | df-mpt 4096 | 
. 2
⊢ (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) = {〈𝑦, 𝑥〉 ∣ (𝑦 ∈ 𝐵 ∧ 𝑥 = (𝑆 × {𝑦}))} | 
| 49 | 41, 47, 48 | 3eqtr4i 2227 | 
1
⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) |