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

Metamath Proof Explorer

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 eqtr3id ⊢ ( 𝜑 → ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) = ( I ↾ 𝐵 ) )
28 27 coeq2d ⊢ ( 𝜑 → ( 𝐴 ∘ ( ( 𝑏 ∈ ( 𝐵 ↑m 1o ) ↦ ( 𝑏 ‘ ∅ ) ) ∘ ( 𝑤 ∈ 𝐵 ↦ ( 1o × { 𝑤 } ) ) ) ) = ( 𝐴 ∘ ( I ↾ 𝐵 ) ) )
29 17 28 eqtrid ⊢ ( 𝜑 → ( ( 𝐴 ∘ ( 𝑏 ∈ ( 𝐵 ↑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 biimtrid ⊢ ( 𝜑 → ( ( ( 𝑎 ∈ 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 biimtrid ⊢ ( 𝜑 → ( ( ( 𝑎 ∈ 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 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 vsnex ⊢ { 𝑓 } ∈ 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 ⊢ ( 𝜑 → 𝜌 )