Theorem imasbas 13395

Description: The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.)

Hypotheses

Ref	Expression
imasbas.u	⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
imasbas.v	⊢ (𝜑 → 𝑉 = (Base‘𝑅))
imasbas.f	⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
imasbas.r	⊢ (𝜑 → 𝑅 ∈ 𝑍)

Assertion

Ref	Expression
imasbas	⊢ (𝜑 → 𝐵 = (Base‘𝑈))

Proof of Theorem imasbas

Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasbas.u	. . . 4 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
2		imasbas.v	. . . 4 ⊢ (𝜑 → 𝑉 = (Base‘𝑅))
3		eqid 2231	. . . 4 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2231	. . . 4 ⊢ (.r‘𝑅) = (.r‘𝑅)
5		eqid 2231	. . . 4 ⊢ ( ·𝑠 ‘𝑅) = ( ·𝑠 ‘𝑅)
6		eqidd 2232	. . . 4 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩})
7		eqidd 2232	. . . 4 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩})
8		imasbas.f	. . . 4 ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)
9		imasbas.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	imasival 13394	. . 3 ⊢ (𝜑 → 𝑈 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩})
11	10	fveq1d 5641	. 2 ⊢ (𝜑 → (𝑈‘(Base‘ndx)) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩}‘(Base‘ndx)))
12		basendxnn 13143	. . . . . 6 ⊢ (Base‘ndx) ∈ ℕ
13		basfn 13146	. . . . . . . . 9 ⊢ Base Fn V
14	9	elexd 2816	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ V)
15		funfvex 5656	. . . . . . . . . 10 ⊢ ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
16	15	funfni 5432	. . . . . . . . 9 ⊢ ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
17	13, 14, 16	sylancr 414	. . . . . . . 8 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
18	2, 17	eqeltrd 2308	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ V)
19		focdmex 6277	. . . . . . 7 ⊢ (𝑉 ∈ V → (𝐹:𝑉–onto→𝐵 → 𝐵 ∈ V))
20	18, 8, 19	sylc 62	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ V)
21		opexg 4320	. . . . . 6 ⊢ (((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ V) → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
22	12, 20, 21	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
23		plusgndxnn 13199	. . . . . 6 ⊢ (+g‘ndx) ∈ ℕ
24		fof 5559	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵)
25	8, 24	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝑉⟶𝐵)
26	25, 18	fexd 5884	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ V)
27		vex 2805	. . . . . . . . . . . . . 14 ⊢ 𝑝 ∈ V
28		fvexg 5658	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ V ∧ 𝑝 ∈ V) → (𝐹‘𝑝) ∈ V)
29	26, 27, 28	sylancl 413	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑝) ∈ V)
30		vex 2805	. . . . . . . . . . . . . 14 ⊢ 𝑞 ∈ V
31		fvexg 5658	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ V ∧ 𝑞 ∈ V) → (𝐹‘𝑞) ∈ V)
32	26, 30, 31	sylancl 413	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝑞) ∈ V)
33		opexg 4320	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑝) ∈ V ∧ (𝐹‘𝑞) ∈ V) → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
34	29, 32, 33	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → ⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V)
35	27	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑝 ∈ V)
36		plusgslid 13200	. . . . . . . . . . . . . . . 16 ⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
37	36	slotex 13114	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ 𝑍 → (+g‘𝑅) ∈ V)
38	9, 37	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (+g‘𝑅) ∈ V)
39	30	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑞 ∈ V)
40		ovexg 6052	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ V ∧ (+g‘𝑅) ∈ V ∧ 𝑞 ∈ V) → (𝑝(+g‘𝑅)𝑞) ∈ V)
41	35, 38, 39, 40	syl3anc 1273	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑝(+g‘𝑅)𝑞) ∈ V)
42		fvexg 5658	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ V ∧ (𝑝(+g‘𝑅)𝑞) ∈ V) → (𝐹‘(𝑝(+g‘𝑅)𝑞)) ∈ V)
43	26, 41, 42	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝑝(+g‘𝑅)𝑞)) ∈ V)
44		opexg 4320	. . . . . . . . . . . 12 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝(+g‘𝑅)𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩ ∈ V)
45	34, 43, 44	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩ ∈ V)
46		snexg 4274	. . . . . . . . . . 11 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩ ∈ V → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
47	45, 46	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
48	47	ralrimivw 2606	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
49		iunexg 6281	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
50	18, 48, 49	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
51	50	ralrimivw 2606	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
52		iunexg 6281	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
53	18, 51, 52	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V)
54		opexg 4320	. . . . . 6 ⊢ (((+g‘ndx) ∈ ℕ ∧ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩} ∈ V) → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩ ∈ V)
55	23, 53, 54	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩ ∈ V)
56		mulrslid 13220	. . . . . . 7 ⊢ (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
57	56	simpri 113	. . . . . 6 ⊢ (.r‘ndx) ∈ ℕ
58	56	slotex 13114	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ 𝑍 → (.r‘𝑅) ∈ V)
59	9, 58	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (.r‘𝑅) ∈ V)
60		ovexg 6052	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ V ∧ (.r‘𝑅) ∈ V ∧ 𝑞 ∈ V) → (𝑝(.r‘𝑅)𝑞) ∈ V)
61	35, 59, 39, 60	syl3anc 1273	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑝(.r‘𝑅)𝑞) ∈ V)
62		fvexg 5658	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ V ∧ (𝑝(.r‘𝑅)𝑞) ∈ V) → (𝐹‘(𝑝(.r‘𝑅)𝑞)) ∈ V)
63	26, 61, 62	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝑝(.r‘𝑅)𝑞)) ∈ V)
64		opexg 4320	. . . . . . . . . . . 12 ⊢ ((⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝(.r‘𝑅)𝑞)) ∈ V) → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩ ∈ V)
65	34, 63, 64	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩ ∈ V)
66		snexg 4274	. . . . . . . . . . 11 ⊢ (⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩ ∈ V → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
67	65, 66	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
68	67	ralrimivw 2606	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
69		iunexg 6281	. . . . . . . . 9 ⊢ ((𝑉 ∈ V ∧ ∀𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
70	18, 68, 69	syl2anc 411	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
71	70	ralrimivw 2606	. . . . . . 7 ⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
72		iunexg 6281	. . . . . . 7 ⊢ ((𝑉 ∈ V ∧ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V) → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
73	18, 71, 72	syl2anc 411	. . . . . 6 ⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V)
74		opexg 4320	. . . . . 6 ⊢ (((.r‘ndx) ∈ ℕ ∧ ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩} ∈ V) → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩ ∈ V)
75	57, 73, 74	sylancr 414	. . . . 5 ⊢ (𝜑 → ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩ ∈ V)
76		tpexg 4541	. . . . 5 ⊢ ((⟨(Base‘ndx), 𝐵⟩ ∈ V ∧ ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩ ∈ V ∧ ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩ ∈ V) → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩} ∈ V)
77	22, 55, 75, 76	syl3anc 1273	. . . 4 ⊢ (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩} ∈ V)
78	10, 77	eqeltrd 2308	. . 3 ⊢ (𝜑 → 𝑈 ∈ V)
79		baseid 13141	. . 3 ⊢ Base = Slot (Base‘ndx)
80	78, 79, 12	strndxid 13115	. 2 ⊢ (𝜑 → (𝑈‘(Base‘ndx)) = (Base‘𝑈))
81	12	a1i 9	. . 3 ⊢ (𝜑 → (Base‘ndx) ∈ ℕ)
82		basendxnplusgndx 13213	. . . 4 ⊢ (Base‘ndx) ≠ (+g‘ndx)
83	82	a1i 9	. . 3 ⊢ (𝜑 → (Base‘ndx) ≠ (+g‘ndx))
84		basendxnmulrndx 13222	. . . 4 ⊢ (Base‘ndx) ≠ (.r‘ndx)
85	84	a1i 9	. . 3 ⊢ (𝜑 → (Base‘ndx) ≠ (.r‘ndx))
86		fvtp1g 5862	. . 3 ⊢ ((((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ V) ∧ ((Base‘ndx) ≠ (+g‘ndx) ∧ (Base‘ndx) ≠ (.r‘ndx))) → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩}‘(Base‘ndx)) = 𝐵)
87	81, 20, 83, 85, 86	syl22anc 1274	. 2 ⊢ (𝜑 → ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(+g‘𝑅)𝑞))⟩}⟩, ⟨(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝(.r‘𝑅)𝑞))⟩}⟩}‘(Base‘ndx)) = 𝐵)
88	11, 80, 87	3eqtr3rd 2273	1 ⊢ (𝜑 → 𝐵 = (Base‘𝑈))

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202   ≠ wne 2402  ∀wral 2510  Vcvv 2802  {csn 3669  {ctp 3671  ⟨cop 3672  ∪ ciun 3970   Fn wfn 5321  ⟶wf 5322  –onto→wfo 5324  ‘cfv 5326  (class class class)co 6018  ℕcn 9143  ndxcnx 13084  Slot cslot 13086  Basecbs 13087  +_gcplusg 13165  ._rcmulr 13166   ·_𝑠 cvsca 13169   “_s cimas 13387

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-pre-ltirr 8144  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-pw 3654  df-sn 3675  df-pr 3676  df-tp 3677  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-ltxr 8219  df-inn 9144  df-2 9202  df-3 9203  df-ndx 13090  df-slot 13091  df-base 13093  df-plusg 13178  df-mulr 13179  df-iimas 13390

This theorem is referenced by:  qusbas  13415  imasmnd2  13540  imasgrp2  13702  imasabl  13928  imasrng  13975  imasring  14083