Metamath Proof Explorer

Theorem fpwrelmapffslem

Description: Lemma for fpwrelmapffs . For this theorem, the sets A and B could be infinite, but the relation R itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fpwrelmapffslem.1 ⊢ 𝐴 ∈ V
fpwrelmapffslem.2 ⊢ 𝐵 ∈ V
fpwrelmapffslem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝒫 𝐵 )
fpwrelmapffslem.4 ⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
Assertion fpwrelmapffslem ( 𝜑 → ( 𝑅 ∈ Fin ↔ ( ran 𝐹 ⊆ Fin ∧ ( 𝐹 supp ∅ ) ∈ Fin ) ) )

Proof

Step Hyp Ref Expression
1 fpwrelmapffslem.1 ⊢ 𝐴 ∈ V
2 fpwrelmapffslem.2 ⊢ 𝐵 ∈ V
3 fpwrelmapffslem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝒫 𝐵 )
4 fpwrelmapffslem.4 ⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
5 relopab ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
6 releq ⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } → ( Rel 𝑅 ↔ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ) )
7 5 6 mpbiri ⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } → Rel 𝑅 )
8 relfi ⊢ ( Rel 𝑅 → ( 𝑅 ∈ Fin ↔ ( dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin ) ) )
9 4 7 8 3syl ⊢ ( 𝜑 → ( 𝑅 ∈ Fin ↔ ( dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin ) ) )
10 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
11 ancom ⊢ ( ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ 𝑧 ) ↔ ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
12 11 exbii ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ 𝑧 ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
13 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
14 eleq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) )
15 13 14 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ 𝑧 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) )
16 12 15 bitr3i ⊢ ( ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) )
17 16 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) )
18 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
19 18 exbii ⊢ ( ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
20 10 17 19 3bitr3ri ⊢ ( ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) )
21 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) )
22 20 21 bitr2i ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
23 22 a1i ⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) ) ) )
24 vex ⊢ 𝑤 ∈ V
25 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) )
26 25 anbi2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
27 26 exbidv ⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) )
28 24 27 elab ⊢ ( 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) )
29 eluniab ⊢ ( 𝑤 ∈ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) ) )
30 23 28 29 3bitr4g ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ↔ 𝑤 ∈ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ) )
31 30 eqrdv ⊢ ( 𝜑 → { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } )
32 31 eleq1d ⊢ ( 𝜑 → ( { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ∈ Fin ↔ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ∈ Fin ↔ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin ) )
34 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝒫 𝐵 → 𝐹 Fn 𝐴 )
35 fnrnfv ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } )
36 3 34 35 3syl ⊢ ( 𝜑 → ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } )
37 36 adantr ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } )
38 0ex ⊢ ∅ ∈ V
39 38 a1i ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ∅ ∈ V )
40 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝒫 𝐵 ∧ 𝐴 ∈ V ) → 𝐹 ∈ V )
41 3 1 40 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
42 41 adantr ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → 𝐹 ∈ V )
43 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
44 43 adantr ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → Fun 𝐹 )
45 opabdm ⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } → dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
46 4 45 syl ⊢ ( 𝜑 → dom 𝑅 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
47 1 40 mpan2 ⊢ ( 𝐹 : 𝐴 ⟶ 𝒫 𝐵 → 𝐹 ∈ V )
48 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ ∅ ∈ V ) → ( 𝐹 supp ∅ ) = ( ◡ 𝐹 “ ( V ∖ { ∅ } ) ) )
49 38 48 mpan2 ⊢ ( 𝐹 ∈ V → ( 𝐹 supp ∅ ) = ( ◡ 𝐹 “ ( V ∖ { ∅ } ) ) )
50 3 47 49 3syl ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) = ( ◡ 𝐹 “ ( V ∖ { ∅ } ) ) )
51 3 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
52 51 cnveqd ⊢ ( 𝜑 → ◡ 𝐹 = ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
53 52 imaeq1d ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ { ∅ } ) ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) “ ( V ∖ { ∅ } ) ) )
54 50 53 eqtrd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) = ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) “ ( V ∖ { ∅ } ) ) )
55 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) )
56 55 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) “ ( V ∖ { ∅ } ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { ∅ } ) }
57 54 56 eqtrdi ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { ∅ } ) } )
58 suppvalfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ ∅ ∈ V ) → ( 𝐹 supp ∅ ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ∅ } )
59 1 38 58 mp3an23 ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 supp ∅ ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ∅ } )
60 3 34 59 3syl ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ∅ } )
61 n0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) )
62 61 rabbii ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ∅ } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) }
63 62 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ∅ } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } )
64 60 57 63 3eqtr3d ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( V ∖ { ∅ } ) } = { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } )
65 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
66 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) )
67 66 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
68 65 67 eqtr4i ⊢ { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) }
69 68 a1i ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ∃ 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
70 57 64 69 3eqtrd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
71 46 70 eqtr4d ⊢ ( 𝜑 → dom 𝑅 = ( 𝐹 supp ∅ ) )
72 71 eleq1d ⊢ ( 𝜑 → ( dom 𝑅 ∈ Fin ↔ ( 𝐹 supp ∅ ) ∈ Fin ) )
73 72 biimpa ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( 𝐹 supp ∅ ) ∈ Fin )
74 39 42 44 73 ffsrn ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ran 𝐹 ∈ Fin )
75 37 74 eqeltrrd ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin )
76 unifi ⊢ ( ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ⊆ Fin ) → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin )
77 76 ex ⊢ ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin → ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ⊆ Fin → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin ) )
78 75 77 syl ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ⊆ Fin → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin ) )
79 unifi3 ⊢ ( ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ⊆ Fin )
80 78 79 impbid1 ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ⊆ Fin ↔ ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ∈ Fin ) )
81 33 80 bitr4d ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ∈ Fin ↔ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ⊆ Fin ) )
82 opabrn ⊢ ( 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } → ran 𝑅 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
83 4 82 syl ⊢ ( 𝜑 → ran 𝑅 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } )
84 83 eleq1d ⊢ ( 𝜑 → ( ran 𝑅 ∈ Fin ↔ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ∈ Fin ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( ran 𝑅 ∈ Fin ↔ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑥 ) ) } ∈ Fin ) )
86 37 sseq1d ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( ran 𝐹 ⊆ Fin ↔ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( 𝐹 ‘ 𝑥 ) } ⊆ Fin ) )
87 81 85 86 3bitr4d ⊢ ( ( 𝜑 ∧ dom 𝑅 ∈ Fin ) → ( ran 𝑅 ∈ Fin ↔ ran 𝐹 ⊆ Fin ) )
88 87 pm5.32da ⊢ ( 𝜑 → ( ( dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin ) ↔ ( dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin ) ) )
89 72 anbi1d ⊢ ( 𝜑 → ( ( dom 𝑅 ∈ Fin ∧ ran 𝐹 ⊆ Fin ) ↔ ( ( 𝐹 supp ∅ ) ∈ Fin ∧ ran 𝐹 ⊆ Fin ) ) )
90 88 89 bitrd ⊢ ( 𝜑 → ( ( dom 𝑅 ∈ Fin ∧ ran 𝑅 ∈ Fin ) ↔ ( ( 𝐹 supp ∅ ) ∈ Fin ∧ ran 𝐹 ⊆ Fin ) ) )
91 ancom ⊢ ( ( ( 𝐹 supp ∅ ) ∈ Fin ∧ ran 𝐹 ⊆ Fin ) ↔ ( ran 𝐹 ⊆ Fin ∧ ( 𝐹 supp ∅ ) ∈ Fin ) )
92 91 a1i ⊢ ( 𝜑 → ( ( ( 𝐹 supp ∅ ) ∈ Fin ∧ ran 𝐹 ⊆ Fin ) ↔ ( ran 𝐹 ⊆ Fin ∧ ( 𝐹 supp ∅ ) ∈ Fin ) ) )
93 9 90 92 3bitrd ⊢ ( 𝜑 → ( 𝑅 ∈ Fin ↔ ( ran 𝐹 ⊆ Fin ∧ ( 𝐹 supp ∅ ) ∈ Fin ) ) )