Theorem imasival 13379

Description: Value of an image structure. The is a lemma for the theorems imasbas 13380, imasplusg 13381, and imasmulr 13382 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)

Hypotheses

Ref	Expression
imasval.u	⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
imasval.v	⊢ (𝜑 → 𝑉 = (Base‘𝑅))
imasval.p	⊢ + = (+g‘𝑅)
imasval.m	⊢ × = (.r‘𝑅)
imasval.q	⊢ · = ( ·𝑠 ‘𝑅)
imasval.a	⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
imasval.t	⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
imasval.f	⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
imasval.r	⊢ (𝜑 → 𝑅 ∈ 𝑍)

Assertion

Ref	Expression
imasival	⊢ (𝜑 → 𝑈 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})

Distinct variable groups:   𝐹,𝑝,𝑞   𝑅,𝑝,𝑞   𝑉,𝑝,𝑞   𝜑,𝑝,𝑞

Allowed substitution hints:   𝐵(𝑞,𝑝)   + (𝑞,𝑝)   ✚ (𝑞,𝑝)   ∙ (𝑞,𝑝)   · (𝑞,𝑝)   × (𝑞,𝑝)   𝑈(𝑞,𝑝)   𝑍(𝑞,𝑝)

Proof of Theorem imasival

Dummy variables 𝑓 𝑟 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasval.u	. 2 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
2		df-iimas 13375	. . . 4 ⊢ “s = (𝑓 ∈ V, 𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑣⦌{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩})
3	2	a1i 9	. . 3 ⊢ (𝜑 → “s = (𝑓 ∈ V, 𝑟 ∈ V ↦ ⦋(Base‘𝑟) / 𝑣⦌{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩}))
4		basfn 13131	. . . . . 6 ⊢ Base Fn V
5		vex 2803	. . . . . 6 ⊢ 𝑟 ∈ V
6		funfvex 5652	. . . . . . 7 ⊢ ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
7	6	funfni 5429	. . . . . 6 ⊢ ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
8	4, 5, 7	mp2an 426	. . . . 5 ⊢ (Base‘𝑟) ∈ V
9	8	a1i 9	. . . 4 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
10		simplrl 535	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
11	10	rneqd 4959	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
12		imasval.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
13		forn 5559	. . . . . . . . 9 ⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵)
14	12, 13	syl 14	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 = 𝐵)
15	14	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
16	11, 15	eqtrd 2262	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
17	16	opeq2d 3867	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
18		simplrr 536	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
19	18	fveq2d 5639	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
20		simpr 110	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
21		imasval.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
22	21	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
23	19, 20, 22	3eqtr4d 2272	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
24	10	fveq1d 5637	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑝) = (𝐹‘𝑝))
25	10	fveq1d 5637	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘𝑞) = (𝐹‘𝑞))
26	24, 25	opeq12d 3868	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩ = ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩)
27	18	fveq2d 5639	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = (+g‘𝑅))
28		imasval.p	. . . . . . . . . . . . . 14 ⊢ + = (+g‘𝑅)
29	27, 28	eqtr4di 2280	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g‘𝑟) = + )
30	29	oveqd 6030	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g‘𝑟)𝑞) = (𝑝 + 𝑞))
31	10, 30	fveq12d 5642	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g‘𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
32	26, 31	opeq12d 3868	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
33	32	sneqd 3680	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
34	23, 33	iuneq12d 3992	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
35	23, 34	iuneq12d 3992	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
36		imasval.a	. . . . . . . 8 ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
37	36	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
38	35, 37	eqtr4d 2265	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩} = ✚ )
39	38	opeq2d 3867	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ✚ ⟩)
40	18	fveq2d 5639	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = (.r‘𝑅))
41		imasval.m	. . . . . . . . . . . . . 14 ⊢ × = (.r‘𝑅)
42	40, 41	eqtr4di 2280	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r‘𝑟) = × )
43	42	oveqd 6030	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r‘𝑟)𝑞) = (𝑝 × 𝑞))
44	10, 43	fveq12d 5642	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r‘𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
45	26, 44	opeq12d 3868	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩ = ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
46	45	sneqd 3680	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
47	23, 46	iuneq12d 3992	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
48	23, 47	iuneq12d 3992	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
49		imasval.t	. . . . . . . 8 ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
50	49	ad2antrr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
51	48, 50	eqtr4d 2265	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩} = ∙ )
52	51	opeq2d 3867	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ∙ ⟩)
53	17, 39, 52	tpeq123d 3761	. . . 4 ⊢ (((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})
54	9, 53	csbied 3172	. . 3 ⊢ ((𝜑 ∧ (𝑓 = 𝐹 ∧ 𝑟 = 𝑅)) → ⦋(Base‘𝑟) / 𝑣⦌{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(+g‘𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑣 ∪ 𝑞 ∈ 𝑣 {⟨⟨(𝑓‘𝑝), (𝑓‘𝑞)⟩, (𝑓‘(𝑝(.r‘𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})
55		fof 5556	. . . . 5 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
56	12, 55	syl 14	. . . 4 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
57		imasval.r	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
58	57	elexd 2814	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ V)
59		funfvex 5652	. . . . . . 7 ⊢ ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
60	59	funfni 5429	. . . . . 6 ⊢ ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
61	4, 58, 60	sylancr 414	. . . . 5 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
62	21, 61	eqeltrd 2306	. . . 4 ⊢ (𝜑 → 𝑉 ∈ V)
63	56, 62	fexd 5879	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
64		basendxnn 13128	. . . . 5 ⊢ (Base‘ndx) ∈ ℕ
65		focdmex 6272	. . . . . 6 ⊢ (𝑉 ∈ V → (𝐹:𝑉–onto→𝐵 → 𝐵 ∈ V))
66	62, 12, 65	sylc 62	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
67		opexg 4318	. . . . 5 ⊢ (((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ V) → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
68	64, 66, 67	sylancr 414	. . . 4 ⊢ (𝜑 → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
69		plusgndxnn 13184	. . . . 5 ⊢ (+g‘ndx) ∈ ℕ
70	63	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → 𝐹 ∈ V)
71		vex 2803	. . . . . . . . . . . . . . 15 ⊢ 𝑝 ∈ V
72	71	a1i 9	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → 𝑝 ∈ V)
73		fvexg 5654	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ V ∧ 𝑝 ∈ V) → (𝐹‘𝑝) ∈ V)
74	70, 72, 73	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑝) ∈ V)
75		vex 2803	. . . . . . . . . . . . . . 15 ⊢ 𝑞 ∈ V
76	75	a1i 9	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → 𝑞 ∈ V)
77		fvexg 5654	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ V ∧ 𝑞 ∈ V) → (𝐹‘𝑞) ∈ V)
78	70, 76, 77	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → (𝐹‘𝑞) ∈ V)
79		opexg 4318	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑝) ∈ V ∧ (𝐹‘𝑞) ∈ V) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
80	74, 78, 79	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
81		plusgslid 13185	. . . . . . . . . . . . . . . . . 18 ⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
82	81	slotex 13099	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ 𝑍 → (+g‘𝑅) ∈ V)
83	57, 82	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (+g‘𝑅) ∈ V)
84	28, 83	eqeltrid 2316	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → + ∈ V)
85	84	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → + ∈ V)
86		ovexg 6047	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ V ∧ + ∈ V ∧ 𝑞 ∈ V) → (𝑝 + 𝑞) ∈ V)
87	72, 85, 76, 86	syl3anc 1271	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → (𝑝 + 𝑞) ∈ V)
88		fvexg 5654	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ V ∧ (𝑝 + 𝑞) ∈ V) → (𝐹‘(𝑝 + 𝑞)) ∈ V)
89	70, 87, 88	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → (𝐹‘(𝑝 + 𝑞)) ∈ V)
90		opexg 4318	. . . . . . . . . . . 12 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 + 𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩ ∈ V)
91	80, 89, 90	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩ ∈ V)
92		snexg 4272	. . . . . . . . . . 11 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩ ∈ V → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
93	91, 92	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
94	93	ralrimiva 2603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
95		iunexg 6276	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
96	62, 94, 95	syl2an2r 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
97	96	ralrimiva 2603	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
98		iunexg 6276	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V) → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
99	62, 97, 98	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
100	36, 99	eqeltrd 2306	. . . . 5 ⊢ (𝜑 → ✚ ∈ V)
101		opexg 4318	. . . . 5 ⊢ (((+g‘ndx) ∈ ℕ ∧ ✚ ∈ V) → ⟨(+g‘ndx), ✚ ⟩ ∈ V)
102	69, 100, 101	sylancr 414	. . . 4 ⊢ (𝜑 → ⟨(+g‘ndx), ✚ ⟩ ∈ V)
103		mulrslid 13205	. . . . . 6 ⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
104	103	simpri 113	. . . . 5 ⊢ (.r‘ndx) ∈ ℕ
105	103	slotex 13099	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ 𝑍 → (.r‘𝑅) ∈ V)
106	57, 105	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (.r‘𝑅) ∈ V)
107	41, 106	eqeltrid 2316	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → × ∈ V)
108	107	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → × ∈ V)
109		ovexg 6047	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ V ∧ × ∈ V ∧ 𝑞 ∈ V) → (𝑝 × 𝑞) ∈ V)
110	72, 108, 76, 109	syl3anc 1271	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → (𝑝 × 𝑞) ∈ V)
111		fvexg 5654	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ V ∧ (𝑝 × 𝑞) ∈ V) → (𝐹‘(𝑝 × 𝑞)) ∈ V)
112	70, 110, 111	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → (𝐹‘(𝑝 × 𝑞)) ∈ V)
113		opexg 4318	. . . . . . . . . . . 12 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 × 𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩ ∈ V)
114	80, 112, 113	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩ ∈ V)
115		snexg 4272	. . . . . . . . . . 11 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩ ∈ V → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
116	114, 115	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑉) ∧ 𝑞 ∈ 𝑉) → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
117	116	ralrimiva 2603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
118		iunexg 6276	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
119	62, 117, 118	syl2an2r 597	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑉) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
120	119	ralrimiva 2603	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
121		iunexg 6276	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V) → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
122	62, 120, 121	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
123	49, 122	eqeltrd 2306	. . . . 5 ⊢ (𝜑 → ∙ ∈ V)
124		opexg 4318	. . . . 5 ⊢ (((.r‘ndx) ∈ ℕ ∧ ∙ ∈ V) → ⟨(.r‘ndx), ∙ ⟩ ∈ V)
125	104, 123, 124	sylancr 414	. . . 4 ⊢ (𝜑 → ⟨(.r‘ndx), ∙ ⟩ ∈ V)
126		tpexg 4539	. . . 4 ⊢ ((⟨(Base‘ndx), 𝐵⟩ ∈ V ∧ ⟨(+g‘ndx), ✚ ⟩ ∈ V ∧ ⟨(.r‘ndx), ∙ ⟩ ∈ V) → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∈ V)
127	68, 102, 125, 126	syl3anc 1271	. . 3 ⊢ (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∈ V)
128	3, 54, 63, 58, 127	ovmpod 6144	. 2 ⊢ (𝜑 → (𝐹 “s 𝑅) = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})
129	1, 128	eqtrd 2262	1 ⊢ (𝜑 → 𝑈 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩})

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  ∀wral 2508  Vcvv 2800  ⦋csb 3125  {csn 3667  {ctp 3669  ⟨cop 3670  ∪ ciun 3968  ran crn 4724   Fn wfn 5319  ⟶wf 5320  –onto→wfo 5322  ‘cfv 5324  (class class class)co 6013   ∈ cmpo 6015  ℕcn 9133  ndxcnx 13069  Slot cslot 13071  Basecbs 13072  +_gcplusg 13150  ._rcmulr 13151   ·_𝑠 cvsca 13154   “_s cimas 13372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4202  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-tp 3675  df-op 3676  df-uni 3892  df-int 3927  df-iun 3970  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-fv 5332  df-ov 6016  df-oprab 6017  df-mpo 6018  df-inn 9134  df-2 9192  df-3 9193  df-ndx 13075  df-slot 13076  df-base 13078  df-plusg 13163  df-mulr 13164  df-iimas 13375

This theorem is referenced by:  imasbas  13380  imasplusg  13381  imasmulr  13382