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

Theorem 2stropg 12581
Description: The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.)
Hypotheses
Ref Expression
2str.g 𝐺 = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩}
2str.e 𝐸 = Slot 𝑁
2str.l 1 < 𝑁
2str.n 𝑁 ∈ β„•
Assertion
Ref Expression
2stropg ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ + = (πΈβ€˜πΊ))

Proof of Theorem 2stropg
StepHypRef Expression
1 2str.e . . 3 𝐸 = Slot 𝑁
2 2str.n . . 3 𝑁 ∈ β„•
31, 2ndxslid 12489 . 2 (𝐸 = Slot (πΈβ€˜ndx) ∧ (πΈβ€˜ndx) ∈ β„•)
4 2str.g . . 3 𝐺 = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩}
5 basendxnn 12520 . . . . . 6 (Baseβ€˜ndx) ∈ β„•
65a1i 9 . . . . 5 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ (Baseβ€˜ndx) ∈ β„•)
7 simpl 109 . . . . 5 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ 𝐡 ∈ 𝑉)
8 opexg 4230 . . . . 5 (((Baseβ€˜ndx) ∈ β„• ∧ 𝐡 ∈ 𝑉) β†’ ⟨(Baseβ€˜ndx), 𝐡⟩ ∈ V)
96, 7, 8syl2anc 411 . . . 4 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ ⟨(Baseβ€˜ndx), 𝐡⟩ ∈ V)
101, 2ndxarg 12487 . . . . . . 7 (πΈβ€˜ndx) = 𝑁
1110, 2eqeltri 2250 . . . . . 6 (πΈβ€˜ndx) ∈ β„•
1211a1i 9 . . . . 5 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ (πΈβ€˜ndx) ∈ β„•)
13 simpr 110 . . . . 5 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ + ∈ π‘Š)
14 opexg 4230 . . . . 5 (((πΈβ€˜ndx) ∈ β„• ∧ + ∈ π‘Š) β†’ ⟨(πΈβ€˜ndx), + ⟩ ∈ V)
1512, 13, 14syl2anc 411 . . . 4 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ ⟨(πΈβ€˜ndx), + ⟩ ∈ V)
16 prexg 4213 . . . 4 ((⟨(Baseβ€˜ndx), 𝐡⟩ ∈ V ∧ ⟨(πΈβ€˜ndx), + ⟩ ∈ V) β†’ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩} ∈ V)
179, 15, 16syl2anc 411 . . 3 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩} ∈ V)
184, 17eqeltrid 2264 . 2 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ 𝐺 ∈ V)
195nnrei 8930 . . . . . 6 (Baseβ€˜ndx) ∈ ℝ
20 2str.l . . . . . . 7 1 < 𝑁
21 basendx 12519 . . . . . . 7 (Baseβ€˜ndx) = 1
2220, 21, 103brtr4i 4035 . . . . . 6 (Baseβ€˜ndx) < (πΈβ€˜ndx)
2319, 22ltneii 8056 . . . . 5 (Baseβ€˜ndx) β‰  (πΈβ€˜ndx)
2423a1i 9 . . . 4 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ (Baseβ€˜ndx) β‰  (πΈβ€˜ndx))
25 funprg 5268 . . . 4 ((((Baseβ€˜ndx) ∈ β„• ∧ (πΈβ€˜ndx) ∈ β„•) ∧ (𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) ∧ (Baseβ€˜ndx) β‰  (πΈβ€˜ndx)) β†’ Fun {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩})
266, 12, 7, 13, 24, 25syl221anc 1249 . . 3 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ Fun {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩})
274funeqi 5239 . . 3 (Fun 𝐺 ↔ Fun {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩})
2826, 27sylibr 134 . 2 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ Fun 𝐺)
29 prid2g 3699 . . . 4 (⟨(πΈβ€˜ndx), + ⟩ ∈ V β†’ ⟨(πΈβ€˜ndx), + ⟩ ∈ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩})
3015, 29syl 14 . . 3 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ ⟨(πΈβ€˜ndx), + ⟩ ∈ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(πΈβ€˜ndx), + ⟩})
3130, 4eleqtrrdi 2271 . 2 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ ⟨(πΈβ€˜ndx), + ⟩ ∈ 𝐺)
323, 18, 28, 31strslfvd 12506 1 ((𝐡 ∈ 𝑉 ∧ + ∈ π‘Š) β†’ + = (πΈβ€˜πΊ))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148   β‰  wne 2347  Vcvv 2739  {cpr 3595  βŸ¨cop 3597   class class class wbr 4005  Fun wfun 5212  β€˜cfv 5218  1c1 7814   < clt 7994  β„•cn 8921  ndxcnx 12461  Slot cslot 12463  Basecbs 12464
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-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7904  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910  ax-pre-ltirr 7925
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-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  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-iota 5180  df-fun 5220  df-fv 5226  df-pnf 7996  df-mnf 7997  df-ltxr 7999  df-inn 8922  df-ndx 12467  df-slot 12468  df-base 12470
This theorem is referenced by:  grpplusgg  12588  eltpsg  13625
  Copyright terms: Public domain W3C validator