| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mptcnfimad.m | . . 3
⊢ 𝑀 = (𝑥 ∈ 𝐴 ↦ (𝐹 “ 𝑥)) | 
| 2 | 1 | cnveqi 5884 | . 2
⊢ ◡𝑀 = ◡(𝑥 ∈ 𝐴 ↦ (𝐹 “ 𝑥)) | 
| 3 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) | 
| 4 |  | mptcnfimad.f | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑊) | 
| 5 |  | f1of 6847 | . . . . . . . . . . . 12
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉⟶𝑊) | 
| 6 | 4, 5 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑉⟶𝑊) | 
| 7 |  | mptcnfimad.v | . . . . . . . . . . 11
⊢ (𝜑 → 𝑉 ∈ 𝑈) | 
| 8 | 6, 7 | fexd 7248 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ V) | 
| 9 | 8 | imaexd 7939 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑥) ∈ V) | 
| 10 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹 “ 𝑥) ∈ V) | 
| 11 | 1, 3, 10 | elrnmpt1d 5974 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹 “ 𝑥) ∈ ran 𝑀) | 
| 12 |  | f1of1 6846 | . . . . . . . . 9
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊) | 
| 13 | 4, 12 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝑉–1-1→𝑊) | 
| 14 |  | mptcnfimad.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑉) | 
| 15 |  | ssel 3976 | . . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝒫 𝑉 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝑉)) | 
| 16 |  | elpwi 4606 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑉 → 𝑥 ⊆ 𝑉) | 
| 17 | 15, 16 | syl6 35 | . . . . . . . . . 10
⊢ (𝐴 ⊆ 𝒫 𝑉 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝑉)) | 
| 18 | 14, 17 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝑉)) | 
| 19 | 18 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝑉) | 
| 20 |  | f1imacnv 6863 | . . . . . . . . 9
⊢ ((𝐹:𝑉–1-1→𝑊 ∧ 𝑥 ⊆ 𝑉) → (◡𝐹 “ (𝐹 “ 𝑥)) = 𝑥) | 
| 21 | 20 | eqcomd 2742 | . . . . . . . 8
⊢ ((𝐹:𝑉–1-1→𝑊 ∧ 𝑥 ⊆ 𝑉) → 𝑥 = (◡𝐹 “ (𝐹 “ 𝑥))) | 
| 22 | 13, 19, 21 | syl2an2r 685 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = (◡𝐹 “ (𝐹 “ 𝑥))) | 
| 23 | 11, 22 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹 “ 𝑥) ∈ ran 𝑀 ∧ 𝑥 = (◡𝐹 “ (𝐹 “ 𝑥)))) | 
| 24 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑦 = (𝐹 “ 𝑥) → (𝑦 ∈ ran 𝑀 ↔ (𝐹 “ 𝑥) ∈ ran 𝑀)) | 
| 25 |  | imaeq2 6073 | . . . . . . . 8
⊢ (𝑦 = (𝐹 “ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (𝐹 “ 𝑥))) | 
| 26 | 25 | eqeq2d 2747 | . . . . . . 7
⊢ (𝑦 = (𝐹 “ 𝑥) → (𝑥 = (◡𝐹 “ 𝑦) ↔ 𝑥 = (◡𝐹 “ (𝐹 “ 𝑥)))) | 
| 27 | 24, 26 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = (𝐹 “ 𝑥) → ((𝑦 ∈ ran 𝑀 ∧ 𝑥 = (◡𝐹 “ 𝑦)) ↔ ((𝐹 “ 𝑥) ∈ ran 𝑀 ∧ 𝑥 = (◡𝐹 “ (𝐹 “ 𝑥))))) | 
| 28 | 23, 27 | syl5ibrcom 247 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹 “ 𝑥) → (𝑦 ∈ ran 𝑀 ∧ 𝑥 = (◡𝐹 “ 𝑦)))) | 
| 29 | 28 | expimpd 453 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹 “ 𝑥)) → (𝑦 ∈ ran 𝑀 ∧ 𝑥 = (◡𝐹 “ 𝑦)))) | 
| 30 | 10 | ralrimiva 3145 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹 “ 𝑥) ∈ V) | 
| 31 | 1 | fnmpt 6707 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 (𝐹 “ 𝑥) ∈ V → 𝑀 Fn 𝐴) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 Fn 𝐴) | 
| 33 |  | fvelrnb 6968 | . . . . . . . . . 10
⊢ (𝑀 Fn 𝐴 → (𝑦 ∈ ran 𝑀 ↔ ∃𝑥 ∈ 𝐴 (𝑀‘𝑥) = 𝑦)) | 
| 34 | 32, 33 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ ran 𝑀 ↔ ∃𝑥 ∈ 𝐴 (𝑀‘𝑥) = 𝑦)) | 
| 35 |  | imaeq2 6073 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐹 “ 𝑥) = (𝐹 “ 𝑧)) | 
| 36 | 35 | cbvmptv 5254 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 ↦ (𝐹 “ 𝑥)) = (𝑧 ∈ 𝐴 ↦ (𝐹 “ 𝑧)) | 
| 37 | 1, 36 | eqtri 2764 | . . . . . . . . . . . . . 14
⊢ 𝑀 = (𝑧 ∈ 𝐴 ↦ (𝐹 “ 𝑧)) | 
| 38 | 37 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑀 = (𝑧 ∈ 𝐴 ↦ (𝐹 “ 𝑧))) | 
| 39 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 = 𝑥) → 𝑧 = 𝑥) | 
| 40 | 39 | imaeq2d 6077 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 = 𝑥) → (𝐹 “ 𝑧) = (𝐹 “ 𝑥)) | 
| 41 | 38, 40, 3, 10 | fvmptd 7022 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑀‘𝑥) = (𝐹 “ 𝑥)) | 
| 42 | 41 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑀‘𝑥) = 𝑦 ↔ (𝐹 “ 𝑥) = 𝑦)) | 
| 43 | 25 | eqcoms 2744 | . . . . . . . . . . . . . 14
⊢ ((𝐹 “ 𝑥) = 𝑦 → (◡𝐹 “ 𝑦) = (◡𝐹 “ (𝐹 “ 𝑥))) | 
| 44 | 43 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 “ 𝑥) = 𝑦) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (𝐹 “ 𝑥))) | 
| 45 | 13, 19, 20 | syl2an2r 685 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ (𝐹 “ 𝑥)) = 𝑥) | 
| 46 | 45, 3 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ (𝐹 “ 𝑥)) ∈ 𝐴) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 “ 𝑥) = 𝑦) → (◡𝐹 “ (𝐹 “ 𝑥)) ∈ 𝐴) | 
| 48 | 44, 47 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 “ 𝑥) = 𝑦) → (◡𝐹 “ 𝑦) ∈ 𝐴) | 
| 49 | 48 | ex 412 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹 “ 𝑥) = 𝑦 → (◡𝐹 “ 𝑦) ∈ 𝐴)) | 
| 50 | 42, 49 | sylbid 240 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑀‘𝑥) = 𝑦 → (◡𝐹 “ 𝑦) ∈ 𝐴)) | 
| 51 | 50 | rexlimdva 3154 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 (𝑀‘𝑥) = 𝑦 → (◡𝐹 “ 𝑦) ∈ 𝐴)) | 
| 52 | 34, 51 | sylbid 240 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ ran 𝑀 → (◡𝐹 “ 𝑦) ∈ 𝐴)) | 
| 53 | 52 | imp 406 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑀) → (◡𝐹 “ 𝑦) ∈ 𝐴) | 
| 54 |  | f1ofo 6854 | . . . . . . . . . 10
⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–onto→𝑊) | 
| 55 | 4, 54 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑉–onto→𝑊) | 
| 56 |  | mptcnfimad.r | . . . . . . . . . . 11
⊢ (𝜑 → ran 𝑀 ⊆ 𝒫 𝑊) | 
| 57 |  | ssel 3976 | . . . . . . . . . . . 12
⊢ (ran
𝑀 ⊆ 𝒫 𝑊 → (𝑦 ∈ ran 𝑀 → 𝑦 ∈ 𝒫 𝑊)) | 
| 58 |  | elpwi 4606 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝒫 𝑊 → 𝑦 ⊆ 𝑊) | 
| 59 | 57, 58 | syl6 35 | . . . . . . . . . . 11
⊢ (ran
𝑀 ⊆ 𝒫 𝑊 → (𝑦 ∈ ran 𝑀 → 𝑦 ⊆ 𝑊)) | 
| 60 | 56, 59 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ ran 𝑀 → 𝑦 ⊆ 𝑊)) | 
| 61 | 60 | imp 406 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑀) → 𝑦 ⊆ 𝑊) | 
| 62 |  | foimacnv 6864 | . . . . . . . . 9
⊢ ((𝐹:𝑉–onto→𝑊 ∧ 𝑦 ⊆ 𝑊) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) | 
| 63 | 55, 61, 62 | syl2an2r 685 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑀) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) | 
| 64 | 63 | eqcomd 2742 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑀) → 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))) | 
| 65 | 53, 64 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑀) → ((◡𝐹 “ 𝑦) ∈ 𝐴 ∧ 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦)))) | 
| 66 |  | eleq1 2828 | . . . . . . 7
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑥 ∈ 𝐴 ↔ (◡𝐹 “ 𝑦) ∈ 𝐴)) | 
| 67 |  | imaeq2 6073 | . . . . . . . 8
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦))) | 
| 68 | 67 | eqeq2d 2747 | . . . . . . 7
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝑦 = (𝐹 “ 𝑥) ↔ 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦)))) | 
| 69 | 66, 68 | anbi12d 632 | . . . . . 6
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹 “ 𝑥)) ↔ ((◡𝐹 “ 𝑦) ∈ 𝐴 ∧ 𝑦 = (𝐹 “ (◡𝐹 “ 𝑦))))) | 
| 70 | 65, 69 | syl5ibrcom 247 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran 𝑀) → (𝑥 = (◡𝐹 “ 𝑦) → (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹 “ 𝑥)))) | 
| 71 | 70 | expimpd 453 | . . . 4
⊢ (𝜑 → ((𝑦 ∈ ran 𝑀 ∧ 𝑥 = (◡𝐹 “ 𝑦)) → (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹 “ 𝑥)))) | 
| 72 | 29, 71 | impbid 212 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹 “ 𝑥)) ↔ (𝑦 ∈ ran 𝑀 ∧ 𝑥 = (◡𝐹 “ 𝑦)))) | 
| 73 | 72 | mptcnv 6158 | . 2
⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ (𝐹 “ 𝑥)) = (𝑦 ∈ ran 𝑀 ↦ (◡𝐹 “ 𝑦))) | 
| 74 | 2, 73 | eqtrid 2788 | 1
⊢ (𝜑 → ◡𝑀 = (𝑦 ∈ ran 𝑀 ↦ (◡𝐹 “ 𝑦))) |