ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imasival GIF version

Theorem imasival 12733
Description: Value of an image structure. The is a lemma for the theorems imasbas 12734, imasplusg 12735, and imasmulr 12736 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.
StepHypRef Expression
1 imasval.u . 2 (𝜑𝑈 = (𝐹s 𝑅))
2 df-iimas 12729 . . . 4 s = (𝑓 ∈ V, 𝑟 ∈ V ↦ (Base‘𝑟) / 𝑣{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩})
32a1i 9 . . 3 (𝜑 → “s = (𝑓 ∈ V, 𝑟 ∈ V ↦ (Base‘𝑟) / 𝑣{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩}))
4 basfn 12523 . . . . . 6 Base Fn V
5 vex 2742 . . . . . 6 𝑟 ∈ V
6 funfvex 5534 . . . . . . 7 ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
76funfni 5318 . . . . . 6 ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
84, 5, 7mp2an 426 . . . . 5 (Base‘𝑟) ∈ V
98a1i 9 . . . 4 ((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
10 simplrl 535 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
1110rneqd 4858 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
12 imasval.f . . . . . . . . 9 (𝜑𝐹:𝑉onto𝐵)
13 forn 5443 . . . . . . . . 9 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
1412, 13syl 14 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐵)
1514ad2antrr 488 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
1611, 15eqtrd 2210 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
1716opeq2d 3787 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
18 simplrr 536 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
1918fveq2d 5521 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
20 simpr 110 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
21 imasval.v . . . . . . . . . 10 (𝜑𝑉 = (Base‘𝑅))
2221ad2antrr 488 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
2319, 20, 223eqtr4d 2220 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
2410fveq1d 5519 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑝) = (𝐹𝑝))
2510fveq1d 5519 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑞) = (𝐹𝑞))
2624, 25opeq12d 3788 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓𝑝), (𝑓𝑞)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
2718fveq2d 5521 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = (+g𝑅))
28 imasval.p . . . . . . . . . . . . . 14 + = (+g𝑅)
2927, 28eqtr4di 2228 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = + )
3029oveqd 5895 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g𝑟)𝑞) = (𝑝 + 𝑞))
3110, 30fveq12d 5524 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
3226, 31opeq12d 3788 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
3332sneqd 3607 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3423, 33iuneq12d 3912 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3523, 34iuneq12d 3912 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
36 imasval.a . . . . . . . 8 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3736ad2antrr 488 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3835, 37eqtr4d 2213 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = )
3938opeq2d 3787 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ⟩)
4018fveq2d 5521 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = (.r𝑅))
41 imasval.m . . . . . . . . . . . . . 14 × = (.r𝑅)
4240, 41eqtr4di 2228 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = × )
4342oveqd 5895 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r𝑟)𝑞) = (𝑝 × 𝑞))
4410, 43fveq12d 5524 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
4526, 44opeq12d 3788 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
4645sneqd 3607 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4723, 46iuneq12d 3912 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4823, 47iuneq12d 3912 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
49 imasval.t . . . . . . . 8 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
5049ad2antrr 488 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
5148, 50eqtr4d 2213 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = )
5251opeq2d 3787 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ⟩)
5317, 39, 52tpeq123d 3686 . . . 4 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
549, 53csbied 3105 . . 3 ((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) → (Base‘𝑟) / 𝑣{⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
55 fof 5440 . . . . 5 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
5612, 55syl 14 . . . 4 (𝜑𝐹:𝑉𝐵)
57 imasval.r . . . . . . 7 (𝜑𝑅𝑍)
5857elexd 2752 . . . . . 6 (𝜑𝑅 ∈ V)
59 funfvex 5534 . . . . . . 7 ((Fun Base ∧ 𝑅 ∈ dom Base) → (Base‘𝑅) ∈ V)
6059funfni 5318 . . . . . 6 ((Base Fn V ∧ 𝑅 ∈ V) → (Base‘𝑅) ∈ V)
614, 58, 60sylancr 414 . . . . 5 (𝜑 → (Base‘𝑅) ∈ V)
6221, 61eqeltrd 2254 . . . 4 (𝜑𝑉 ∈ V)
6356, 62fexd 5749 . . 3 (𝜑𝐹 ∈ V)
64 basendxnn 12521 . . . . 5 (Base‘ndx) ∈ ℕ
65 focdmex 6119 . . . . . 6 (𝑉 ∈ V → (𝐹:𝑉onto𝐵𝐵 ∈ V))
6662, 12, 65sylc 62 . . . . 5 (𝜑𝐵 ∈ V)
67 opexg 4230 . . . . 5 (((Base‘ndx) ∈ ℕ ∧ 𝐵 ∈ V) → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
6864, 66, 67sylancr 414 . . . 4 (𝜑 → ⟨(Base‘ndx), 𝐵⟩ ∈ V)
69 plusgndxnn 12573 . . . . 5 (+g‘ndx) ∈ ℕ
7063ad2antrr 488 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → 𝐹 ∈ V)
71 vex 2742 . . . . . . . . . . . . . . 15 𝑝 ∈ V
7271a1i 9 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → 𝑝 ∈ V)
73 fvexg 5536 . . . . . . . . . . . . . 14 ((𝐹 ∈ V ∧ 𝑝 ∈ V) → (𝐹𝑝) ∈ V)
7470, 72, 73syl2anc 411 . . . . . . . . . . . . 13 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → (𝐹𝑝) ∈ V)
75 vex 2742 . . . . . . . . . . . . . . 15 𝑞 ∈ V
7675a1i 9 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → 𝑞 ∈ V)
77 fvexg 5536 . . . . . . . . . . . . . 14 ((𝐹 ∈ V ∧ 𝑞 ∈ V) → (𝐹𝑞) ∈ V)
7870, 76, 77syl2anc 411 . . . . . . . . . . . . 13 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → (𝐹𝑞) ∈ V)
79 opexg 4230 . . . . . . . . . . . . 13 (((𝐹𝑝) ∈ V ∧ (𝐹𝑞) ∈ V) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ V)
8074, 78, 79syl2anc 411 . . . . . . . . . . . 12 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ V)
81 plusgslid 12574 . . . . . . . . . . . . . . . . . 18 (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
8281slotex 12492 . . . . . . . . . . . . . . . . 17 (𝑅𝑍 → (+g𝑅) ∈ V)
8357, 82syl 14 . . . . . . . . . . . . . . . 16 (𝜑 → (+g𝑅) ∈ V)
8428, 83eqeltrid 2264 . . . . . . . . . . . . . . 15 (𝜑+ ∈ V)
8584ad2antrr 488 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → + ∈ V)
86 ovexg 5912 . . . . . . . . . . . . . 14 ((𝑝 ∈ V ∧ + ∈ V ∧ 𝑞 ∈ V) → (𝑝 + 𝑞) ∈ V)
8772, 85, 76, 86syl3anc 1238 . . . . . . . . . . . . 13 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → (𝑝 + 𝑞) ∈ V)
88 fvexg 5536 . . . . . . . . . . . . 13 ((𝐹 ∈ V ∧ (𝑝 + 𝑞) ∈ V) → (𝐹‘(𝑝 + 𝑞)) ∈ V)
8970, 87, 88syl2anc 411 . . . . . . . . . . . 12 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → (𝐹‘(𝑝 + 𝑞)) ∈ V)
90 opexg 4230 . . . . . . . . . . . 12 ((⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 + 𝑞)) ∈ V) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩ ∈ V)
9180, 89, 90syl2anc 411 . . . . . . . . . . 11 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩ ∈ V)
92 snexg 4186 . . . . . . . . . . 11 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩ ∈ V → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
9391, 92syl 14 . . . . . . . . . 10 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
9493ralrimiva 2550 . . . . . . . . 9 ((𝜑𝑝𝑉) → ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
95 iunexg 6123 . . . . . . . . 9 ((𝑉 ∈ V ∧ ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V) → 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
9662, 94, 95syl2an2r 595 . . . . . . . 8 ((𝜑𝑝𝑉) → 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
9796ralrimiva 2550 . . . . . . 7 (𝜑 → ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
98 iunexg 6123 . . . . . . 7 ((𝑉 ∈ V ∧ ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V) → 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
9962, 97, 98syl2anc 411 . . . . . 6 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩} ∈ V)
10036, 99eqeltrd 2254 . . . . 5 (𝜑 ∈ V)
101 opexg 4230 . . . . 5 (((+g‘ndx) ∈ ℕ ∧ ∈ V) → ⟨(+g‘ndx), ⟩ ∈ V)
10269, 100, 101sylancr 414 . . . 4 (𝜑 → ⟨(+g‘ndx), ⟩ ∈ V)
103 mulrslid 12593 . . . . . 6 (.r = Slot (.r‘ndx) ∧ (.r‘ndx) ∈ ℕ)
104103simpri 113 . . . . 5 (.r‘ndx) ∈ ℕ
105103slotex 12492 . . . . . . . . . . . . . . . . 17 (𝑅𝑍 → (.r𝑅) ∈ V)
10657, 105syl 14 . . . . . . . . . . . . . . . 16 (𝜑 → (.r𝑅) ∈ V)
10741, 106eqeltrid 2264 . . . . . . . . . . . . . . 15 (𝜑× ∈ V)
108107ad2antrr 488 . . . . . . . . . . . . . 14 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → × ∈ V)
109 ovexg 5912 . . . . . . . . . . . . . 14 ((𝑝 ∈ V ∧ × ∈ V ∧ 𝑞 ∈ V) → (𝑝 × 𝑞) ∈ V)
11072, 108, 76, 109syl3anc 1238 . . . . . . . . . . . . 13 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → (𝑝 × 𝑞) ∈ V)
111 fvexg 5536 . . . . . . . . . . . . 13 ((𝐹 ∈ V ∧ (𝑝 × 𝑞) ∈ V) → (𝐹‘(𝑝 × 𝑞)) ∈ V)
11270, 110, 111syl2anc 411 . . . . . . . . . . . 12 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → (𝐹‘(𝑝 × 𝑞)) ∈ V)
113 opexg 4230 . . . . . . . . . . . 12 ((⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ V ∧ (𝐹‘(𝑝 × 𝑞)) ∈ V) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩ ∈ V)
11480, 112, 113syl2anc 411 . . . . . . . . . . 11 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩ ∈ V)
115 snexg 4186 . . . . . . . . . . 11 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩ ∈ V → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
116114, 115syl 14 . . . . . . . . . 10 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
117116ralrimiva 2550 . . . . . . . . 9 ((𝜑𝑝𝑉) → ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
118 iunexg 6123 . . . . . . . . 9 ((𝑉 ∈ V ∧ ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V) → 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
11962, 117, 118syl2an2r 595 . . . . . . . 8 ((𝜑𝑝𝑉) → 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
120119ralrimiva 2550 . . . . . . 7 (𝜑 → ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
121 iunexg 6123 . . . . . . 7 ((𝑉 ∈ V ∧ ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V) → 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
12262, 120, 121syl2anc 411 . . . . . 6 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩} ∈ V)
12349, 122eqeltrd 2254 . . . . 5 (𝜑 ∈ V)
124 opexg 4230 . . . . 5 (((.r‘ndx) ∈ ℕ ∧ ∈ V) → ⟨(.r‘ndx), ⟩ ∈ V)
125104, 123, 124sylancr 414 . . . 4 (𝜑 → ⟨(.r‘ndx), ⟩ ∈ V)
126 tpexg 4446 . . . 4 ((⟨(Base‘ndx), 𝐵⟩ ∈ V ∧ ⟨(+g‘ndx), ⟩ ∈ V ∧ ⟨(.r‘ndx), ⟩ ∈ V) → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∈ V)
12768, 102, 125, 126syl3anc 1238 . . 3 (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∈ V)
1283, 54, 63, 58, 127ovmpod 6005 . 2 (𝜑 → (𝐹s 𝑅) = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
1291, 128eqtrd 2210 1 (𝜑𝑈 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353  wcel 2148  wral 2455  Vcvv 2739  csb 3059  {csn 3594  {ctp 3596  cop 3597   ciun 3888  ran crn 4629   Fn wfn 5213  wf 5214  ontowfo 5216  cfv 5218  (class class class)co 5878  cmpo 5880  cn 8922  ndxcnx 12462  Slot cslot 12464  Basecbs 12465  +gcplusg 12539  .rcmulr 12540   ·𝑠 cvsca 12543  s cimas 12726
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7905  ax-resscn 7906  ax-1re 7908  ax-addrcl 7911
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-tp 3602  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5881  df-oprab 5882  df-mpo 5883  df-inn 8923  df-2 8981  df-3 8982  df-ndx 12468  df-slot 12469  df-base 12471  df-plusg 12552  df-mulr 12553  df-iimas 12729
This theorem is referenced by:  imasbas  12734  imasplusg  12735  imasmulr  12736
  Copyright terms: Public domain W3C validator