Theorem pf1ind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pf1ind.cb	⊢ 𝐵 = ( Base ‘ 𝑅 )
	pf1ind.cp	⊢ + = ( +g ‘ 𝑅 )
	pf1ind.ct	⊢ · = ( .r ‘ 𝑅 )
	pf1ind.cq	⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
	pf1ind.ad	⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑄 ∧ 𝜏 ) ∧ ( 𝑔 ∈ 𝑄 ∧ 𝜂 ) ) ) → 𝜁 )
	pf1ind.mu	⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑄 ∧ 𝜏 ) ∧ ( 𝑔 ∈ 𝑄 ∧ 𝜂 ) ) ) → 𝜎 )
	pf1ind.wa	⊢ ( 𝑥 = ( 𝐵 × { 𝑓 } ) → ( 𝜓 ↔ 𝜒 ) )
	pf1ind.wb	⊢ ( 𝑥 = ( I ↾ 𝐵 ) → ( 𝜓 ↔ 𝜃 ) )
	pf1ind.wc	⊢ ( 𝑥 = 𝑓 → ( 𝜓 ↔ 𝜏 ) )
	pf1ind.wd	⊢ ( 𝑥 = 𝑔 → ( 𝜓 ↔ 𝜂 ) )
	pf1ind.we	⊢ ( 𝑥 = ( 𝑓 ∘f + 𝑔 ) → ( 𝜓 ↔ 𝜁 ) )
	pf1ind.wf	⊢ ( 𝑥 = ( 𝑓 ∘f · 𝑔 ) → ( 𝜓 ↔ 𝜎 ) )
	pf1ind.wg	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜌 ) )
	pf1ind.co	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → 𝜒 )
	pf1ind.pr	⊢ ( 𝜑 → 𝜃 )
	pf1ind.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑄 )
Assertion	pf1ind	⊢ ( 𝜑 → 𝜌 )

Proof

Step	Hyp	Ref	Expression
1		pf1ind.cb	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		pf1ind.cp	⊢ + = ( +g ‘ 𝑅 )
3		pf1ind.ct	⊢ · = ( .r ‘ 𝑅 )
4		pf1ind.cq	⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
5		pf1ind.ad	⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑄 ∧ 𝜏 ) ∧ ( 𝑔 ∈ 𝑄 ∧ 𝜂 ) ) ) → 𝜁 )
6		pf1ind.mu	⊢ ( ( 𝜑 ∧ ( ( 𝑓 ∈ 𝑄 ∧ 𝜏 ) ∧ ( 𝑔 ∈ 𝑄 ∧ 𝜂 ) ) ) → 𝜎 )
7		pf1ind.wa	⊢ ( 𝑥 = ( 𝐵 × { 𝑓 } ) → ( 𝜓 ↔ 𝜒 ) )
8		pf1ind.wb	⊢ ( 𝑥 = ( I ↾ 𝐵 ) → ( 𝜓 ↔ 𝜃 ) )
9		pf1ind.wc	⊢ ( 𝑥 = 𝑓 → ( 𝜓 ↔ 𝜏 ) )
10		pf1ind.wd	⊢ ( 𝑥 = 𝑔 → ( 𝜓 ↔ 𝜂 ) )
11		pf1ind.we	⊢ ( 𝑥 = ( 𝑓 ∘f + 𝑔 ) → ( 𝜓 ↔ 𝜁 ) )
12		pf1ind.wf	⊢ ( 𝑥 = ( 𝑓 ∘f · 𝑔 ) → ( 𝜓 ↔ 𝜎 ) )
13		pf1ind.wg	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜌 ) )
14		pf1ind.co	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → 𝜒 )
15		pf1ind.pr	⊢ ( 𝜑 → 𝜃 )
16		pf1ind.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑄 )
17		coass	⊢ ( ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( 𝐴 ∘ ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
18		df1o2	⊢ 1o = { ∅ }
19	1	fvexi	⊢ 𝐵 ∈ V
20		0ex	⊢ ∅ ∈ V
21		eqid	⊢ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) = ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) )
22	18 19 20 21	mapsncnv	⊢ ◡ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) = ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) )
23	22	coeq2i	⊢ ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ◡ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) = ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) )
24	18 19 20 21	mapsnf1o2	⊢ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) : ( 𝐵 ↑m 1o ) –1-1-onto→ 𝐵
25		f1ococnv2	⊢ ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) : ( 𝐵 ↑m 1o ) –1-1-onto→ 𝐵 → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ◡ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) = ( I ↾ 𝐵 ) )
26	24 25	mp1i	⊢ ( 𝜑 → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ◡ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) = ( I ↾ 𝐵 ) )
27	23 26	syl5eqr	⊢ ( 𝜑 → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( I ↾ 𝐵 ) )
28	27	coeq2d	⊢ ( 𝜑 → ( 𝐴 ∘ ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) = ( 𝐴 ∘ ( I ↾ 𝐵 ) ) )
29	17 28	syl5eq	⊢ ( 𝜑 → ( ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( 𝐴 ∘ ( I ↾ 𝐵 ) ) )
30	4 1	pf1f	⊢ ( 𝐴 ∈ 𝑄 → 𝐴 : 𝐵 ⟶ 𝐵 )
31		fcoi1	⊢ ( 𝐴 : 𝐵 ⟶ 𝐵 → ( 𝐴 ∘ ( I ↾ 𝐵 ) ) = 𝐴 )
32	16 30 31	3syl	⊢ ( 𝜑 → ( 𝐴 ∘ ( I ↾ 𝐵 ) ) = 𝐴 )
33	29 32	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = 𝐴 )
34		eqid	⊢ ( 1o eval 𝑅 ) = ( 1o eval 𝑅 )
35	34 1	evlval	⊢ ( 1o eval 𝑅 ) = ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
36	35	rneqi	⊢ ran ( 1o eval 𝑅 ) = ran ( ( 1o evalSub 𝑅 ) ‘ 𝐵 )
37		an4	⊢ ( ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ ( 𝑏 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) ↔ ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ∧ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
38		eqid	⊢ ran ( 1o eval 𝑅 ) = ran ( 1o eval 𝑅 )
39	4 1 38	mpfpf1	⊢ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) → ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ 𝑄 )
40	4 1 38	mpfpf1	⊢ ( 𝑏 ∈ ran ( 1o eval 𝑅 ) → ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ 𝑄 )
41		vex	⊢ 𝑓 ∈ V
42	41 9	elab	⊢ ( 𝑓 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜏 )
43		eleq1	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝑓 ∈ { 𝑥 ∣ 𝜓 } ↔ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
44	42 43	bitr3id	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝜏 ↔ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
45	44	anbi1d	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( 𝜏 ∧ 𝜂 ) ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ) )
46	45	anbi1d	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( 𝜏 ∧ 𝜂 ) ∧ 𝜑 ) ↔ ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ∧ 𝜑 ) ) )
47		ovex	⊢ ( 𝑓 ∘f + 𝑔 ) ∈ V
48	47 11	elab	⊢ ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜁 )
49		oveq1	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝑓 ∘f + 𝑔 ) = ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + 𝑔 ) )
50	49	eleq1d	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( 𝑓 ∘f + 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) )
51	48 50	bitr3id	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝜁 ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) )
52	46 51	imbi12d	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( ( 𝜏 ∧ 𝜂 ) ∧ 𝜑 ) → 𝜁 ) ↔ ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
53		vex	⊢ 𝑔 ∈ V
54	53 10	elab	⊢ ( 𝑔 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜂 )
55		eleq1	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝑔 ∈ { 𝑥 ∣ 𝜓 } ↔ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
56	54 55	bitr3id	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝜂 ↔ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
57	56	anbi2d	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
58	57	anbi1d	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ∧ 𝜑 ) ↔ ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ 𝜑 ) ) )
59		oveq2	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + 𝑔 ) = ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) )
60	59	eleq1d	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
61	58 60	imbi12d	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
62	5	expcom	⊢ ( ( ( 𝑓 ∈ 𝑄 ∧ 𝜏 ) ∧ ( 𝑔 ∈ 𝑄 ∧ 𝜂 ) ) → ( 𝜑 → 𝜁 ) )
63	62	an4s	⊢ ( ( ( 𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄 ) ∧ ( 𝜏 ∧ 𝜂 ) ) → ( 𝜑 → 𝜁 ) )
64	63	expimpd	⊢ ( ( 𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄 ) → ( ( ( 𝜏 ∧ 𝜂 ) ∧ 𝜑 ) → 𝜁 ) )
65	52 61 64	vtocl2ga	⊢ ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ 𝑄 ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ 𝑄 ) → ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
66	39 40 65	syl2an	⊢ ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) → ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
67	66	expcomd	⊢ ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) → ( 𝜑 → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
68	67	impcom	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
69	36 1	mpff	⊢ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) → 𝑎 : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
70	69	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → 𝑎 : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
71	70	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → 𝑎 Fn ( 𝐵 ↑m 1o ) )
72	36 1	mpff	⊢ ( 𝑏 ∈ ran ( 1o eval 𝑅 ) → 𝑏 : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
73	72	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → 𝑏 : ( 𝐵 ↑m 1o ) ⟶ 𝐵 )
74	73	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → 𝑏 Fn ( 𝐵 ↑m 1o ) )
75		eqid	⊢ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) = ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) )
76	18 19 20 75	mapsnf1o3	⊢ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o )
77		f1of	⊢ ( ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o ) → ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
78	76 77	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
79		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( 𝐵 ↑m 1o ) ∈ V )
80	19	a1i	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → 𝐵 ∈ V )
81		inidm	⊢ ( ( 𝐵 ↑m 1o ) ∩ ( 𝐵 ↑m 1o ) ) = ( 𝐵 ↑m 1o )
82	71 74 78 79 79 80 81	ofco	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) )
83	82	eleq1d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f + ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
84	68 83	sylibrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) → ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
85	84	expimpd	⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ∧ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) → ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
86	37 85	syl5bi	⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ ( 𝑏 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) → ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
87	86	imp	⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ ( 𝑏 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) ) → ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } )
88		ovex	⊢ ( 𝑓 ∘f · 𝑔 ) ∈ V
89	88 12	elab	⊢ ( ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜎 )
90		oveq1	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝑓 ∘f · 𝑔 ) = ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · 𝑔 ) )
91	90	eleq1d	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( 𝑓 ∘f · 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) )
92	89 91	bitr3id	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( 𝜎 ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) )
93	46 92	imbi12d	⊢ ( 𝑓 = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( ( 𝜏 ∧ 𝜂 ) ∧ 𝜑 ) → 𝜎 ) ↔ ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
94		oveq2	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · 𝑔 ) = ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) )
95	94	eleq1d	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
96	58 95	imbi12d	⊢ ( 𝑔 = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) → ( ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝜂 ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · 𝑔 ) ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
97	6	expcom	⊢ ( ( ( 𝑓 ∈ 𝑄 ∧ 𝜏 ) ∧ ( 𝑔 ∈ 𝑄 ∧ 𝜂 ) ) → ( 𝜑 → 𝜎 ) )
98	97	an4s	⊢ ( ( ( 𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄 ) ∧ ( 𝜏 ∧ 𝜂 ) ) → ( 𝜑 → 𝜎 ) )
99	98	expimpd	⊢ ( ( 𝑓 ∈ 𝑄 ∧ 𝑔 ∈ 𝑄 ) → ( ( ( 𝜏 ∧ 𝜂 ) ∧ 𝜑 ) → 𝜎 ) )
100	93 96 99	vtocl2ga	⊢ ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ 𝑄 ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ 𝑄 ) → ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
101	39 40 100	syl2an	⊢ ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) → ( ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ 𝜑 ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
102	101	expcomd	⊢ ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) → ( 𝜑 → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) )
103	102	impcom	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) → ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
104	71 74 78 79 79 80 81	ofco	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) )
105	104	eleq1d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∘f · ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
106	103 105	sylibrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ) → ( ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) → ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
107	106	expimpd	⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ 𝑏 ∈ ran ( 1o eval 𝑅 ) ) ∧ ( ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) → ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
108	37 107	syl5bi	⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ ( 𝑏 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) → ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
109	108	imp	⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ∧ ( 𝑏 ∈ ran ( 1o eval 𝑅 ) ∧ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) ) ) → ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } )
110		coeq1	⊢ ( 𝑦 = ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) → ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
111	110	eleq1d	⊢ ( 𝑦 = ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) → ( ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
112		coeq1	⊢ ( 𝑦 = ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) → ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
113	112	eleq1d	⊢ ( 𝑦 = ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) → ( ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
114		coeq1	⊢ ( 𝑦 = 𝑎 → ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
115	114	eleq1d	⊢ ( 𝑦 = 𝑎 → ( ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( 𝑎 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
116		coeq1	⊢ ( 𝑦 = 𝑏 → ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
117	116	eleq1d	⊢ ( 𝑦 = 𝑏 → ( ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( 𝑏 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
118		coeq1	⊢ ( 𝑦 = ( 𝑎 ∘f + 𝑏 ) → ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
119	118	eleq1d	⊢ ( 𝑦 = ( 𝑎 ∘f + 𝑏 ) → ( ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘f + 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
120		coeq1	⊢ ( 𝑦 = ( 𝑎 ∘f · 𝑏 ) → ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
121	120	eleq1d	⊢ ( 𝑦 = ( 𝑎 ∘f · 𝑏 ) → ( ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑎 ∘f · 𝑏 ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
122		coeq1	⊢ ( 𝑦 = ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) → ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
123	122	eleq1d	⊢ ( 𝑦 = ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) → ( ( 𝑦 ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
124	4	pf1rcl	⊢ ( 𝐴 ∈ 𝑄 → 𝑅 ∈ CRing )
125	16 124	syl	⊢ ( 𝜑 → 𝑅 ∈ CRing )
126	125	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑅 ∈ CRing )
127		1on	⊢ 1o ∈ On
128		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
129	128	mplassa	⊢ ( ( 1o ∈ On ∧ 𝑅 ∈ CRing ) → ( 1o mPoly 𝑅 ) ∈ AssAlg )
130	127 125 129	sylancr	⊢ ( 𝜑 → ( 1o mPoly 𝑅 ) ∈ AssAlg )
131		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
132		eqid	⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
133	131 132	ply1ascl	⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( 1o mPoly 𝑅 ) )
134		eqid	⊢ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) = ( Scalar ‘ ( 1o mPoly 𝑅 ) )
135	133 134	asclrhm	⊢ ( ( 1o mPoly 𝑅 ) ∈ AssAlg → ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( ( Scalar ‘ ( 1o mPoly 𝑅 ) ) RingHom ( 1o mPoly 𝑅 ) ) )
136	130 135	syl	⊢ ( 𝜑 → ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( ( Scalar ‘ ( 1o mPoly 𝑅 ) ) RingHom ( 1o mPoly 𝑅 ) ) )
137	127	a1i	⊢ ( 𝜑 → 1o ∈ On )
138	128 137 125	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 1o mPoly 𝑅 ) ) )
139	138	oveq1d	⊢ ( 𝜑 → ( 𝑅 RingHom ( 1o mPoly 𝑅 ) ) = ( ( Scalar ‘ ( 1o mPoly 𝑅 ) ) RingHom ( 1o mPoly 𝑅 ) ) )
140	136 139	eleqtrrd	⊢ ( 𝜑 → ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( 𝑅 RingHom ( 1o mPoly 𝑅 ) ) )
141		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
142	1 141	rhmf	⊢ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( 𝑅 RingHom ( 1o mPoly 𝑅 ) ) → ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) : 𝐵 ⟶ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
143	140 142	syl	⊢ ( 𝜑 → ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) : 𝐵 ⟶ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
144	143	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) )
145		eqid	⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
146	145 34 1 128 141	evl1val	⊢ ( ( 𝑅 ∈ CRing ∧ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
147	126 144 146	syl2anc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( eval1 ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) = ( ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
148	145 131 1 132	evl1sca	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑎 ∈ 𝐵 ) → ( ( eval1 ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) = ( 𝐵 × { 𝑎 } ) )
149	125 148	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( eval1 ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) = ( 𝐵 × { 𝑎 } ) )
150	1	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
151	126 150	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
152	151	oveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 1o mPoly 𝑅 ) )
153	152	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly 𝑅 ) ) )
154	153 133	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) )
155	154	fveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑎 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) )
156	155	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑎 ) ) = ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) )
157		eqid	⊢ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) = ( 1o mPoly ( 𝑅 ↾s 𝐵 ) )
158		eqid	⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
159		eqid	⊢ ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) )
160	127	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 1o ∈ On )
161		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
162	1	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
163	125 161 162	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
164	163	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
165		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
166	35 157 158 1 159 160 126 164 165	evlssca	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( 1o mPoly ( 𝑅 ↾s 𝐵 ) ) ) ‘ 𝑎 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) )
167	156 166	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) = ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) )
168	167	coeq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 1o eval 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
169	147 149 168	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐵 × { 𝑎 } ) = ( ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
170		snex	⊢ { 𝑓 } ∈ V
171	19 170	xpex	⊢ ( 𝐵 × { 𝑓 } ) ∈ V
172	171 7	elab	⊢ ( ( 𝐵 × { 𝑓 } ) ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜒 )
173	14 172	sylibr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐵 ) → ( 𝐵 × { 𝑓 } ) ∈ { 𝑥 ∣ 𝜓 } )
174	173	ralrimiva	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ( 𝐵 × { 𝑓 } ) ∈ { 𝑥 ∣ 𝜓 } )
175		sneq	⊢ ( 𝑓 = 𝑎 → { 𝑓 } = { 𝑎 } )
176	175	xpeq2d	⊢ ( 𝑓 = 𝑎 → ( 𝐵 × { 𝑓 } ) = ( 𝐵 × { 𝑎 } ) )
177	176	eleq1d	⊢ ( 𝑓 = 𝑎 → ( ( 𝐵 × { 𝑓 } ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( 𝐵 × { 𝑎 } ) ∈ { 𝑥 ∣ 𝜓 } ) )
178	177	rspccva	⊢ ( ( ∀ 𝑓 ∈ 𝐵 ( 𝐵 × { 𝑓 } ) ∈ { 𝑥 ∣ 𝜓 } ∧ 𝑎 ∈ 𝐵 ) → ( 𝐵 × { 𝑎 } ) ∈ { 𝑥 ∣ 𝜓 } )
179	174 178	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐵 × { 𝑎 } ) ∈ { 𝑥 ∣ 𝜓 } )
180	169 179	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( ( 𝐵 ↑m 1o ) × { 𝑎 } ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } )
181		resiexg	⊢ ( 𝐵 ∈ V → ( I ↾ 𝐵 ) ∈ V )
182	19 181	ax-mp	⊢ ( I ↾ 𝐵 ) ∈ V
183	182 8	elab	⊢ ( ( I ↾ 𝐵 ) ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜃 )
184	15 183	sylibr	⊢ ( 𝜑 → ( I ↾ 𝐵 ) ∈ { 𝑥 ∣ 𝜓 } )
185	27 184	eqeltrd	⊢ ( 𝜑 → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } )
186		el1o	⊢ ( 𝑎 ∈ 1o ↔ 𝑎 = ∅ )
187		fveq2	⊢ ( 𝑎 = ∅ → ( 𝑏 ‘ 𝑎 ) = ( 𝑏 ‘ ∅ ) )
188	186 187	sylbi	⊢ ( 𝑎 ∈ 1o → ( 𝑏 ‘ 𝑎 ) = ( 𝑏 ‘ ∅ ) )
189	188	mpteq2dv	⊢ ( 𝑎 ∈ 1o → ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) = ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) )
190	189	coeq1d	⊢ ( 𝑎 ∈ 1o → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) )
191	190	eleq1d	⊢ ( 𝑎 ∈ 1o → ( ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ↔ ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
192	185 191	syl5ibrcom	⊢ ( 𝜑 → ( 𝑎 ∈ 1o → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } ) )
193	192	imp	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 1o ) → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ 𝑎 ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } )
194	4 1 38	pf1mpf	⊢ ( 𝐴 ∈ 𝑄 → ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∈ ran ( 1o eval 𝑅 ) )
195	16 194	syl	⊢ ( 𝜑 → ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∈ ran ( 1o eval 𝑅 ) )
196	1 2 3 36 87 109 111 113 115 117 119 121 123 180 193 195	mpfind	⊢ ( 𝜑 → ( ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ∈ { 𝑥 ∣ 𝜓 } )
197	33 196	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ { 𝑥 ∣ 𝜓 } )
198	13	elabg	⊢ ( 𝐴 ∈ 𝑄 → ( 𝐴 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜌 ) )
199	16 198	syl	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜌 ) )
200	197 199	mpbid	⊢ ( 𝜑 → 𝜌 )