This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasaddfnlem

Description: The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasaddf.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
imasaddflem.a ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
Assertion imasaddfnlem ( 𝜑 → ∙ Fn ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imasaddf.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
2 imasaddf.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
3 imasaddflem.a ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
4 opex ⊢ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ V
5 fvex ⊢ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ V
6 4 5 relsnop ⊢ Rel { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ }
7 6 rgenw ⊢ ∀ 𝑞 ∈ 𝑉 Rel { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ }
8 reliun ⊢ ( Rel ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ↔ ∀ 𝑞 ∈ 𝑉 Rel { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
9 7 8 mpbir ⊢ Rel ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ }
10 9 rgenw ⊢ ∀ 𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ }
11 reliun ⊢ ( Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ↔ ∀ 𝑝 ∈ 𝑉 Rel ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
12 10 11 mpbir ⊢ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ }
13 3 releqd ⊢ ( 𝜑 → ( Rel ∙ ↔ Rel ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ) )
14 12 13 mpbiri ⊢ ( 𝜑 → Rel ∙ )
15 fof ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 : 𝑉 ⟶ 𝐵 )
16 1 15 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 ⟶ 𝐵 )
17 ffvelcdm ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ 𝑝 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝐵 )
18 ffvelcdm ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ 𝑞 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 )
19 17 18 anim12dan ⊢ ( ( 𝐹 : 𝑉 ⟶ 𝐵 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 ) )
20 16 19 sylan ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 ) )
21 opelxpi ⊢ ( ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐵 ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐵 × 𝐵 ) )
22 20 21 syl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐵 × 𝐵 ) )
23 opelxpi ⊢ ( ( ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ∈ V ) → ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ ∈ ( ( 𝐵 × 𝐵 ) × V ) )
24 22 5 23 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ ∈ ( ( 𝐵 × 𝐵 ) × V ) )
25 24 snssd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
26 25 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑉 ) ∧ 𝑞 ∈ 𝑉 ) → { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
27 26 iunssd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑉 ) → ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
28 27 iunssd ⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
29 3 28 eqsstrd ⊢ ( 𝜑 → ∙ ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
30 dmss ⊢ ( ∙ ⊆ ( ( 𝐵 × 𝐵 ) × V ) → dom ∙ ⊆ dom ( ( 𝐵 × 𝐵 ) × V ) )
31 29 30 syl ⊢ ( 𝜑 → dom ∙ ⊆ dom ( ( 𝐵 × 𝐵 ) × V ) )
32 vn0 ⊢ V ≠ ∅
33 dmxp ⊢ ( V ≠ ∅ → dom ( ( 𝐵 × 𝐵 ) × V ) = ( 𝐵 × 𝐵 ) )
34 32 33 ax-mp ⊢ dom ( ( 𝐵 × 𝐵 ) × V ) = ( 𝐵 × 𝐵 )
35 31 34 sseqtrdi ⊢ ( 𝜑 → dom ∙ ⊆ ( 𝐵 × 𝐵 ) )
36 forn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
37 1 36 syl ⊢ ( 𝜑 → ran 𝐹 = 𝐵 )
38 37 sqxpeqd ⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐹 ) = ( 𝐵 × 𝐵 ) )
39 35 38 sseqtrrd ⊢ ( 𝜑 → dom ∙ ⊆ ( ran 𝐹 × ran 𝐹 ) )
40 3 eleq2d ⊢ ( 𝜑 → ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∙ ↔ ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∙ ↔ ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ) )
42 df-br ⊢ ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 ↔ ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∙ )
43 eliun ⊢ ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ↔ ∃ 𝑝 ∈ 𝑉 ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
44 eliun ⊢ ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ↔ ∃ 𝑞 ∈ 𝑉 ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
45 44 rexbii ⊢ ( ∃ 𝑝 ∈ 𝑉 ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ↔ ∃ 𝑝 ∈ 𝑉 ∃ 𝑞 ∈ 𝑉 ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
46 43 45 bitr2i ⊢ ( ∃ 𝑝 ∈ 𝑉 ∃ 𝑞 ∈ 𝑉 ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ↔ ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } )
47 41 42 46 3bitr4g ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 ↔ ∃ 𝑝 ∈ 𝑉 ∃ 𝑞 ∈ 𝑉 ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ) )
48 opex ⊢ ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ V
49 48 elsn ⊢ ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ↔ ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ = ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ )
50 opex ⊢ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∈ V
51 vex ⊢ 𝑤 ∈ V
52 50 51 opth ⊢ ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ = ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ ↔ ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∧ 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
53 fvex ⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
54 fvex ⊢ ( 𝐹 ‘ 𝑏 ) ∈ V
55 53 54 opth ⊢ ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ↔ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) )
56 55 2 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
57 eqeq2 ⊢ ( ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) → ( 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ↔ 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) )
58 57 biimprd ⊢ ( ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) → ( 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
59 56 58 syl6 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ → ( 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) ) )
60 59 impd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∧ 𝑤 = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
61 52 60 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ = ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
62 49 61 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
63 62 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
64 63 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ∃ 𝑝 ∈ 𝑉 ∃ 𝑞 ∈ 𝑉 ⟨ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ , 𝑤 ⟩ ∈ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
65 47 64 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
66 65 alrimiv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ∀ 𝑤 ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) )
67 mo2icl ⊢ ( ∀ 𝑤 ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 → 𝑤 = ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) ) → ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 )
68 66 67 syl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 )
69 68 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 )
70 fofn ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → 𝐹 Fn 𝑉 )
71 1 70 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
72 opeq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑏 ) → ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ = ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ )
73 72 breq1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑏 ) → ( ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ↔ ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 ) )
74 73 mobidv ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑏 ) → ( ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ↔ ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 ) )
75 74 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ↔ ∀ 𝑏 ∈ 𝑉 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 ) )
76 71 75 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ↔ ∀ 𝑏 ∈ 𝑉 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 ) )
77 76 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ∙ 𝑤 ) )
78 69 77 mpbird ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 )
79 opeq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ )
80 79 breq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 ↔ ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ) )
81 80 mobidv ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ∃* 𝑤 ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 ↔ ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ) )
82 81 ralbidv ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 ↔ ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ) )
83 82 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ) )
84 71 83 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ ( 𝐹 ‘ 𝑎 ) , 𝑧 ⟩ ∙ 𝑤 ) )
85 78 84 mpbird ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 )
86 breq1 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∙ 𝑤 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 ) )
87 86 mobidv ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∃* 𝑤 𝑥 ∙ 𝑤 ↔ ∃* 𝑤 ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 ) )
88 87 ralxp ⊢ ( ∀ 𝑥 ∈ ( ran 𝐹 × ran 𝐹 ) ∃* 𝑤 𝑥 ∙ 𝑤 ↔ ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ∃* 𝑤 ⟨ 𝑦 , 𝑧 ⟩ ∙ 𝑤 )
89 85 88 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ran 𝐹 × ran 𝐹 ) ∃* 𝑤 𝑥 ∙ 𝑤 )
90 ssralv ⊢ ( dom ∙ ⊆ ( ran 𝐹 × ran 𝐹 ) → ( ∀ 𝑥 ∈ ( ran 𝐹 × ran 𝐹 ) ∃* 𝑤 𝑥 ∙ 𝑤 → ∀ 𝑥 ∈ dom ∙ ∃* 𝑤 𝑥 ∙ 𝑤 ) )
91 39 89 90 sylc ⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ∙ ∃* 𝑤 𝑥 ∙ 𝑤 )
92 dffun7 ⊢ ( Fun ∙ ↔ ( Rel ∙ ∧ ∀ 𝑥 ∈ dom ∙ ∃* 𝑤 𝑥 ∙ 𝑤 ) )
93 14 91 92 sylanbrc ⊢ ( 𝜑 → Fun ∙ )
94 eqimss2 ⊢ ( ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ )
95 3 94 syl ⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ )
96 iunss ⊢ ( ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ ↔ ∀ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ )
97 95 96 sylib ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ )
98 iunss ⊢ ( ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ ↔ ∀ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ )
99 opex ⊢ ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ ∈ V
100 99 snss ⊢ ( ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ ∈ ∙ ↔ { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ )
101 4 5 opeldm ⊢ ( ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ ∈ ∙ → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
102 100 101 sylbir ⊢ ( { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ → ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
103 102 ralimi ⊢ ( ∀ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ → ∀ 𝑞 ∈ 𝑉 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
104 98 103 sylbi ⊢ ( ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ → ∀ 𝑞 ∈ 𝑉 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
105 104 ralimi ⊢ ( ∀ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ⊆ ∙ → ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑉 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
106 97 105 syl ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑉 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ )
107 opeq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑞 ) → ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ )
108 107 eleq1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑞 ) → ( ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ↔ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
109 108 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑧 ∈ ran 𝐹 ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ↔ ∀ 𝑞 ∈ 𝑉 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
110 71 109 syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐹 ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ↔ ∀ 𝑞 ∈ 𝑉 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
111 110 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑝 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ↔ ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑉 ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ ∈ dom ∙ ) )
112 106 111 mpbird ⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ )
113 opeq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ )
114 113 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ dom ∙ ↔ ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ) )
115 114 ralbidv ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑝 ) → ( ∀ 𝑧 ∈ ran 𝐹 ⟨ 𝑦 , 𝑧 ⟩ ∈ dom ∙ ↔ ∀ 𝑧 ∈ ran 𝐹 ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ) )
116 115 ralrn ⊢ ( 𝐹 Fn 𝑉 → ( ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ⟨ 𝑦 , 𝑧 ⟩ ∈ dom ∙ ↔ ∀ 𝑝 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ) )
117 71 116 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ⟨ 𝑦 , 𝑧 ⟩ ∈ dom ∙ ↔ ∀ 𝑝 ∈ 𝑉 ∀ 𝑧 ∈ ran 𝐹 ⟨ ( 𝐹 ‘ 𝑝 ) , 𝑧 ⟩ ∈ dom ∙ ) )
118 112 117 mpbird ⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ⟨ 𝑦 , 𝑧 ⟩ ∈ dom ∙ )
119 eleq1 ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ dom ∙ ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ dom ∙ ) )
120 119 ralxp ⊢ ( ∀ 𝑥 ∈ ( ran 𝐹 × ran 𝐹 ) 𝑥 ∈ dom ∙ ↔ ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐹 ⟨ 𝑦 , 𝑧 ⟩ ∈ dom ∙ )
121 118 120 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ran 𝐹 × ran 𝐹 ) 𝑥 ∈ dom ∙ )
122 dfss3 ⊢ ( ( ran 𝐹 × ran 𝐹 ) ⊆ dom ∙ ↔ ∀ 𝑥 ∈ ( ran 𝐹 × ran 𝐹 ) 𝑥 ∈ dom ∙ )
123 121 122 sylibr ⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐹 ) ⊆ dom ∙ )
124 38 123 eqsstrrd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ⊆ dom ∙ )
125 35 124 eqssd ⊢ ( 𝜑 → dom ∙ = ( 𝐵 × 𝐵 ) )
126 df-fn ⊢ ( ∙ Fn ( 𝐵 × 𝐵 ) ↔ ( Fun ∙ ∧ dom ∙ = ( 𝐵 × 𝐵 ) ) )
127 93 125 126 sylanbrc ⊢ ( 𝜑 → ∙ Fn ( 𝐵 × 𝐵 ) )