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 ( 𝐵 × 𝐵 ) )