| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fpwrelmapffslem.4 | . . 3
⊢ (𝜑 → 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) | 
| 2 |  | relopabv 5831 | . . . 4
⊢ Rel
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} | 
| 3 |  | releq 5786 | . . . 4
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → (Rel 𝑅 ↔ Rel {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))})) | 
| 4 | 2, 3 | mpbiri 258 | . . 3
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → Rel 𝑅) | 
| 5 |  | relfi 32615 | . . 3
⊢ (Rel
𝑅 → (𝑅 ∈ Fin ↔ (dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin))) | 
| 6 | 1, 4, 5 | 3syl 18 | . 2
⊢ (𝜑 → (𝑅 ∈ Fin ↔ (dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin))) | 
| 7 |  | rexcom4 3288 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥))) | 
| 8 |  | ancom 460 | . . . . . . . . . . . . . . . 16
⊢ ((𝑧 = (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) ↔ (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥))) | 
| 9 | 8 | exbii 1848 | . . . . . . . . . . . . . . 15
⊢
(∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥))) | 
| 10 |  | fvex 6919 | . . . . . . . . . . . . . . . 16
⊢ (𝐹‘𝑥) ∈ V | 
| 11 |  | eleq2 2830 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝐹‘𝑥) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ (𝐹‘𝑥))) | 
| 12 | 10, 11 | ceqsexv 3532 | . . . . . . . . . . . . . . 15
⊢
(∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) ↔ 𝑤 ∈ (𝐹‘𝑥)) | 
| 13 | 9, 12 | bitr3i 277 | . . . . . . . . . . . . . 14
⊢
(∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ 𝑤 ∈ (𝐹‘𝑥)) | 
| 14 | 13 | rexbii 3094 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐴 ∃𝑧(𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ (𝐹‘𝑥)) | 
| 15 |  | r19.42v 3191 | . . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ (𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) | 
| 16 | 15 | exbii 1848 | . . . . . . . . . . . . 13
⊢
(∃𝑧∃𝑥 ∈ 𝐴 (𝑤 ∈ 𝑧 ∧ 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) | 
| 17 | 7, 14, 16 | 3bitr3ri 302 | . . . . . . . . . . . 12
⊢
(∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑤 ∈ (𝐹‘𝑥)) | 
| 18 |  | df-rex 3071 | . . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 𝑤 ∈ (𝐹‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥))) | 
| 19 | 17, 18 | bitr2i 276 | . . . . . . . . . . 11
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) | 
| 20 | 19 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)) ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)))) | 
| 21 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑤 ∈ V | 
| 22 |  | eleq1w 2824 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑤 ∈ (𝐹‘𝑥))) | 
| 23 | 22 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)))) | 
| 24 | 23 | exbidv 1921 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥)))) | 
| 25 | 21, 24 | elab 3679 | . . . . . . . . . 10
⊢ (𝑤 ∈ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ (𝐹‘𝑥))) | 
| 26 |  | eluniab 4921 | . . . . . . . . . 10
⊢ (𝑤 ∈ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ↔ ∃𝑧(𝑤 ∈ 𝑧 ∧ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥))) | 
| 27 | 20, 25, 26 | 3bitr4g 314 | . . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ↔ 𝑤 ∈ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)})) | 
| 28 | 27 | eqrdv 2735 | . . . . . . . 8
⊢ (𝜑 → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) | 
| 29 | 28 | eleq1d 2826 | . . . . . . 7
⊢ (𝜑 → ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin ↔ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) | 
| 30 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin ↔ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) | 
| 31 |  | fpwrelmapffslem.3 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶𝒫 𝐵) | 
| 32 |  | ffn 6736 | . . . . . . . . . . 11
⊢ (𝐹:𝐴⟶𝒫 𝐵 → 𝐹 Fn 𝐴) | 
| 33 |  | fnrnfv 6968 | . . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) | 
| 34 | 31, 32, 33 | 3syl 18 | . . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) | 
| 35 | 34 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)}) | 
| 36 |  | 0ex 5307 | . . . . . . . . . . 11
⊢ ∅
∈ V | 
| 37 | 36 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ∅ ∈
V) | 
| 38 |  | fpwrelmapffslem.1 | . . . . . . . . . . . 12
⊢ 𝐴 ∈ V | 
| 39 |  | fex 7246 | . . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝒫 𝐵 ∧ 𝐴 ∈ V) → 𝐹 ∈ V) | 
| 40 | 31, 38, 39 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ V) | 
| 41 | 40 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → 𝐹 ∈ V) | 
| 42 | 31 | ffund 6740 | . . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) | 
| 43 | 42 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → Fun 𝐹) | 
| 44 |  | opabdm 32623 | . . . . . . . . . . . . . 14
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → dom 𝑅 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) | 
| 45 | 1, 44 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝑅 = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) | 
| 46 | 38, 39 | mpan2 691 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐴⟶𝒫 𝐵 → 𝐹 ∈ V) | 
| 47 |  | suppimacnv 8199 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ V ∧ ∅ ∈
V) → (𝐹 supp ∅)
= (◡𝐹 “ (V ∖
{∅}))) | 
| 48 | 36, 47 | mpan2 691 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ V → (𝐹 supp ∅) = (◡𝐹 “ (V ∖
{∅}))) | 
| 49 | 31, 46, 48 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 supp ∅) = (◡𝐹 “ (V ∖
{∅}))) | 
| 50 | 31 | feqmptd 6977 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | 
| 51 | 50 | cnveqd 5886 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ◡𝐹 = ◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) | 
| 52 | 51 | imaeq1d 6077 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝐹 “ (V ∖ {∅})) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ (V ∖
{∅}))) | 
| 53 | 49, 52 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp ∅) = (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ (V ∖
{∅}))) | 
| 54 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) | 
| 55 | 54 | mptpreima 6258 | . . . . . . . . . . . . . . 15
⊢ (◡(𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) “ (V ∖ {∅})) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ (V ∖
{∅})} | 
| 56 | 53, 55 | eqtrdi 2793 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ (V ∖
{∅})}) | 
| 57 |  | suppvalfn 8193 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ ∅ ∈ V) →
(𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅}) | 
| 58 | 38, 36, 57 | mp3an23 1455 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn 𝐴 → (𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅}) | 
| 59 | 31, 32, 58 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp ∅) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅}) | 
| 60 |  | n0 4353 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)) | 
| 61 | 60 | rabbii 3442 | . . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} | 
| 62 | 61 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}) | 
| 63 | 59, 56, 62 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ (V ∖ {∅})} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}) | 
| 64 |  | df-rab 3437 | . . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} | 
| 65 |  | 19.42v 1953 | . . . . . . . . . . . . . . . . 17
⊢
(∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))) | 
| 66 | 65 | abbii 2809 | . . . . . . . . . . . . . . . 16
⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))} | 
| 67 | 64, 66 | eqtr4i 2768 | . . . . . . . . . . . . . . 15
⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} | 
| 68 | 67 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) | 
| 69 | 56, 63, 68 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp ∅) = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) | 
| 70 | 45, 69 | eqtr4d 2780 | . . . . . . . . . . . 12
⊢ (𝜑 → dom 𝑅 = (𝐹 supp ∅)) | 
| 71 | 70 | eleq1d 2826 | . . . . . . . . . . 11
⊢ (𝜑 → (dom 𝑅 ∈ Fin ↔ (𝐹 supp ∅) ∈ Fin)) | 
| 72 | 71 | biimpa 476 | . . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (𝐹 supp ∅) ∈ Fin) | 
| 73 | 37, 41, 43, 72 | ffsrn 32740 | . . . . . . . . 9
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ran 𝐹 ∈ Fin) | 
| 74 | 35, 73 | eqeltrrd 2842 | . . . . . . . 8
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin) | 
| 75 |  | unifi 9384 | . . . . . . . . 9
⊢ (({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin ∧ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin) → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin) | 
| 76 | 75 | ex 412 | . . . . . . . 8
⊢ ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) | 
| 77 | 74, 76 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) | 
| 78 |  | unifi3 32724 | . . . . . . 7
⊢ (∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin) | 
| 79 | 77, 78 | impbid1 225 | . . . . . 6
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin ↔ ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝐹‘𝑥)} ∈ Fin)) | 
| 80 | 30, 79 | bitr4d 282 | . . . . 5
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin ↔ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin)) | 
| 81 |  | opabrn 32624 | . . . . . . . 8
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} → ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) | 
| 82 | 1, 81 | syl 17 | . . . . . . 7
⊢ (𝜑 → ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) | 
| 83 | 82 | eleq1d 2826 | . . . . . 6
⊢ (𝜑 → (ran 𝑅 ∈ Fin ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin)) | 
| 84 | 83 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝑅 ∈ Fin ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ∈ Fin)) | 
| 85 | 35 | sseq1d 4015 | . . . . 5
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝐹 ⊆ Fin ↔ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝐹‘𝑥)} ⊆ Fin)) | 
| 86 | 80, 84, 85 | 3bitr4d 311 | . . . 4
⊢ ((𝜑 ∧ dom 𝑅 ∈ Fin) → (ran 𝑅 ∈ Fin ↔ ran 𝐹 ⊆ Fin)) | 
| 87 | 86 | pm5.32da 579 | . . 3
⊢ (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin) ↔ (dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin))) | 
| 88 | 71 | anbi1d 631 | . . 3
⊢ (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin) ↔ ((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin))) | 
| 89 | 87, 88 | bitrd 279 | . 2
⊢ (𝜑 → ((dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin) ↔ ((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin))) | 
| 90 |  | ancom 460 | . . 3
⊢ (((𝐹 supp ∅) ∈ Fin ∧
ran 𝐹 ⊆ Fin) ↔
(ran 𝐹 ⊆ Fin ∧
(𝐹 supp ∅) ∈
Fin)) | 
| 91 | 90 | a1i 11 | . 2
⊢ (𝜑 → (((𝐹 supp ∅) ∈ Fin ∧ ran 𝐹 ⊆ Fin) ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈
Fin))) | 
| 92 | 6, 89, 91 | 3bitrd 305 | 1
⊢ (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈
Fin))) |