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

Theorem 1stconst 5781
Description: The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008.)
Assertion
Ref Expression
1stconst (B 𝑉 → (1st ↾ (A × {B})):(A × {B})–1-1-ontoA)

Proof of Theorem 1stconst
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snmg 3476 . . 3 (B 𝑉x x {B})
2 fo1stresm 5727 . . 3 (x x {B} → (1st ↾ (A × {B})):(A × {B})–ontoA)
31, 2syl 14 . 2 (B 𝑉 → (1st ↾ (A × {B})):(A × {B})–ontoA)
4 moeq 2710 . . . . . 6 ∃*x x = ⟨y, B
54moani 1967 . . . . 5 ∃*x(y A x = ⟨y, B⟩)
6 vex 2554 . . . . . . . 8 y V
76brres 4560 . . . . . . 7 (x(1st ↾ (A × {B}))y ↔ (x1st y x (A × {B})))
8 fo1st 5723 . . . . . . . . . . 11 1st :V–onto→V
9 fofn 5049 . . . . . . . . . . 11 (1st :V–onto→V → 1st Fn V)
108, 9ax-mp 7 . . . . . . . . . 10 1st Fn V
11 vex 2554 . . . . . . . . . 10 x V
12 fnbrfvb 5155 . . . . . . . . . 10 ((1st Fn V x V) → ((1stx) = yx1st y))
1310, 11, 12mp2an 402 . . . . . . . . 9 ((1stx) = yx1st y)
1413anbi1i 431 . . . . . . . 8 (((1stx) = y x (A × {B})) ↔ (x1st y x (A × {B})))
15 elxp7 5736 . . . . . . . . . . 11 (x (A × {B}) ↔ (x (V × V) ((1stx) A (2ndx) {B})))
16 eleq1 2097 . . . . . . . . . . . . . . 15 ((1stx) = y → ((1stx) Ay A))
1716biimpa 280 . . . . . . . . . . . . . 14 (((1stx) = y (1stx) A) → y A)
1817adantrr 448 . . . . . . . . . . . . 13 (((1stx) = y ((1stx) A (2ndx) {B})) → y A)
1918adantrl 447 . . . . . . . . . . . 12 (((1stx) = y (x (V × V) ((1stx) A (2ndx) {B}))) → y A)
20 elsni 3390 . . . . . . . . . . . . . 14 ((2ndx) {B} → (2ndx) = B)
21 eqopi 5737 . . . . . . . . . . . . . . 15 ((x (V × V) ((1stx) = y (2ndx) = B)) → x = ⟨y, B⟩)
2221an12s 499 . . . . . . . . . . . . . 14 (((1stx) = y (x (V × V) (2ndx) = B)) → x = ⟨y, B⟩)
2320, 22sylanr2 385 . . . . . . . . . . . . 13 (((1stx) = y (x (V × V) (2ndx) {B})) → x = ⟨y, B⟩)
2423adantrrl 455 . . . . . . . . . . . 12 (((1stx) = y (x (V × V) ((1stx) A (2ndx) {B}))) → x = ⟨y, B⟩)
2519, 24jca 290 . . . . . . . . . . 11 (((1stx) = y (x (V × V) ((1stx) A (2ndx) {B}))) → (y A x = ⟨y, B⟩))
2615, 25sylan2b 271 . . . . . . . . . 10 (((1stx) = y x (A × {B})) → (y A x = ⟨y, B⟩))
2726adantl 262 . . . . . . . . 9 ((B 𝑉 ((1stx) = y x (A × {B}))) → (y A x = ⟨y, B⟩))
28 simprr 484 . . . . . . . . . . . 12 ((B 𝑉 (y A x = ⟨y, B⟩)) → x = ⟨y, B⟩)
2928fveq2d 5123 . . . . . . . . . . 11 ((B 𝑉 (y A x = ⟨y, B⟩)) → (1stx) = (1st ‘⟨y, B⟩))
30 simprl 483 . . . . . . . . . . . 12 ((B 𝑉 (y A x = ⟨y, B⟩)) → y A)
31 simpl 102 . . . . . . . . . . . 12 ((B 𝑉 (y A x = ⟨y, B⟩)) → B 𝑉)
32 op1stg 5716 . . . . . . . . . . . 12 ((y A B 𝑉) → (1st ‘⟨y, B⟩) = y)
3330, 31, 32syl2anc 391 . . . . . . . . . . 11 ((B 𝑉 (y A x = ⟨y, B⟩)) → (1st ‘⟨y, B⟩) = y)
3429, 33eqtrd 2069 . . . . . . . . . 10 ((B 𝑉 (y A x = ⟨y, B⟩)) → (1stx) = y)
35 snidg 3391 . . . . . . . . . . . . 13 (B 𝑉B {B})
3635adantr 261 . . . . . . . . . . . 12 ((B 𝑉 (y A x = ⟨y, B⟩)) → B {B})
37 opelxpi 4318 . . . . . . . . . . . 12 ((y A B {B}) → ⟨y, B (A × {B}))
3830, 36, 37syl2anc 391 . . . . . . . . . . 11 ((B 𝑉 (y A x = ⟨y, B⟩)) → ⟨y, B (A × {B}))
3928, 38eqeltrd 2111 . . . . . . . . . 10 ((B 𝑉 (y A x = ⟨y, B⟩)) → x (A × {B}))
4034, 39jca 290 . . . . . . . . 9 ((B 𝑉 (y A x = ⟨y, B⟩)) → ((1stx) = y x (A × {B})))
4127, 40impbida 528 . . . . . . . 8 (B 𝑉 → (((1stx) = y x (A × {B})) ↔ (y A x = ⟨y, B⟩)))
4214, 41syl5bbr 183 . . . . . . 7 (B 𝑉 → ((x1st y x (A × {B})) ↔ (y A x = ⟨y, B⟩)))
437, 42syl5bb 181 . . . . . 6 (B 𝑉 → (x(1st ↾ (A × {B}))y ↔ (y A x = ⟨y, B⟩)))
4443mobidv 1933 . . . . 5 (B 𝑉 → (∃*x x(1st ↾ (A × {B}))y∃*x(y A x = ⟨y, B⟩)))
455, 44mpbiri 157 . . . 4 (B 𝑉∃*x x(1st ↾ (A × {B}))y)
4645alrimiv 1751 . . 3 (B 𝑉y∃*x x(1st ↾ (A × {B}))y)
47 funcnv2 4900 . . 3 (Fun (1st ↾ (A × {B})) ↔ y∃*x x(1st ↾ (A × {B}))y)
4846, 47sylibr 137 . 2 (B 𝑉 → Fun (1st ↾ (A × {B})))
49 dff1o3 5073 . 2 ((1st ↾ (A × {B})):(A × {B})–1-1-ontoA ↔ ((1st ↾ (A × {B})):(A × {B})–ontoA Fun (1st ↾ (A × {B}))))
503, 48, 49sylanbrc 394 1 (B 𝑉 → (1st ↾ (A × {B})):(A × {B})–1-1-ontoA)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1240   = wceq 1242  wex 1378   wcel 1390  ∃*wmo 1898  Vcvv 2551  {csn 3366  cop 3369   class class class wbr 3754   × cxp 4285  ccnv 4286  cres 4289  Fun wfun 4838   Fn wfn 4839  ontowfo 4842  1-1-ontowf1o 4843  cfv 4844  1st c1st 5704  2nd c2nd 5705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3865  ax-pow 3917  ax-pr 3934  ax-un 4135
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3352  df-sn 3372  df-pr 3373  df-op 3375  df-uni 3571  df-iun 3649  df-br 3755  df-opab 3809  df-mpt 3810  df-id 4020  df-xp 4293  df-rel 4294  df-cnv 4295  df-co 4296  df-dm 4297  df-rn 4298  df-res 4299  df-ima 4300  df-iota 4809  df-fun 4846  df-fn 4847  df-f 4848  df-f1 4849  df-fo 4850  df-f1o 4851  df-fv 4852  df-1st 5706  df-2nd 5707
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator