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

Theorem funopg 4880
Description: A Kuratowski ordered pair is a function only if its components are equal. (Contributed by NM, 5-Jun-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
funopg ((A 𝑉 B 𝑊 Fun ⟨A, B⟩) → A = B)

Proof of Theorem funopg
Dummy variables u 𝑡 v w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 3543 . . . . 5 (u = A → ⟨u, 𝑡⟩ = ⟨A, 𝑡⟩)
21funeqd 4869 . . . 4 (u = A → (Fun ⟨u, 𝑡⟩ ↔ Fun ⟨A, 𝑡⟩))
3 eqeq1 2046 . . . 4 (u = A → (u = 𝑡A = 𝑡))
42, 3imbi12d 223 . . 3 (u = A → ((Fun ⟨u, 𝑡⟩ → u = 𝑡) ↔ (Fun ⟨A, 𝑡⟩ → A = 𝑡)))
5 opeq2 3544 . . . . 5 (𝑡 = B → ⟨A, 𝑡⟩ = ⟨A, B⟩)
65funeqd 4869 . . . 4 (𝑡 = B → (Fun ⟨A, 𝑡⟩ ↔ Fun ⟨A, B⟩))
7 eqeq2 2049 . . . 4 (𝑡 = B → (A = 𝑡A = B))
86, 7imbi12d 223 . . 3 (𝑡 = B → ((Fun ⟨A, 𝑡⟩ → A = 𝑡) ↔ (Fun ⟨A, B⟩ → A = B)))
9 funrel 4865 . . . . 5 (Fun ⟨u, 𝑡⟩ → Rel ⟨u, 𝑡⟩)
10 vex 2557 . . . . . 6 u V
11 vex 2557 . . . . . 6 𝑡 V
1210, 11relop 4432 . . . . 5 (Rel ⟨u, 𝑡⟩ ↔ xy(u = {x} 𝑡 = {x, y}))
139, 12sylib 127 . . . 4 (Fun ⟨u, 𝑡⟩ → xy(u = {x} 𝑡 = {x, y}))
1410, 11opth 3968 . . . . . . . 8 (⟨u, 𝑡⟩ = ⟨{x}, {x, y}⟩ ↔ (u = {x} 𝑡 = {x, y}))
15 vex 2557 . . . . . . . . . . . 12 x V
1615opid 3561 . . . . . . . . . . 11 x, x⟩ = {{x}}
1716preq1i 3444 . . . . . . . . . 10 {⟨x, x⟩, {{x}, {x, y}}} = {{{x}}, {{x}, {x, y}}}
18 vex 2557 . . . . . . . . . . . 12 y V
1915, 18dfop 3542 . . . . . . . . . . 11 x, y⟩ = {{x}, {x, y}}
2019preq2i 3445 . . . . . . . . . 10 {⟨x, x⟩, ⟨x, y⟩} = {⟨x, x⟩, {{x}, {x, y}}}
21 snexgOLD 3929 . . . . . . . . . . . 12 (x V → {x} V)
2215, 21ax-mp 7 . . . . . . . . . . 11 {x} V
23 zfpair2 3939 . . . . . . . . . . 11 {x, y} V
2422, 23dfop 3542 . . . . . . . . . 10 ⟨{x}, {x, y}⟩ = {{{x}}, {{x}, {x, y}}}
2517, 20, 243eqtr4ri 2071 . . . . . . . . 9 ⟨{x}, {x, y}⟩ = {⟨x, x⟩, ⟨x, y⟩}
2625eqeq2i 2050 . . . . . . . 8 (⟨u, 𝑡⟩ = ⟨{x}, {x, y}⟩ ↔ ⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩})
2714, 26bitr3i 175 . . . . . . 7 ((u = {x} 𝑡 = {x, y}) ↔ ⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩})
28 dffun4 4859 . . . . . . . . 9 (Fun ⟨u, 𝑡⟩ ↔ (Rel ⟨u, 𝑡 zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v)))
2928simprbi 260 . . . . . . . 8 (Fun ⟨u, 𝑡⟩ → zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v))
3015, 15opex 3960 . . . . . . . . . . 11 x, x V
3130prid1 3470 . . . . . . . . . 10 x, x {⟨x, x⟩, ⟨x, y⟩}
32 eleq2 2101 . . . . . . . . . 10 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → (⟨x, xu, 𝑡⟩ ↔ ⟨x, x {⟨x, x⟩, ⟨x, y⟩}))
3331, 32mpbiri 157 . . . . . . . . 9 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → ⟨x, xu, 𝑡⟩)
3415, 18opex 3960 . . . . . . . . . . 11 x, y V
3534prid2 3471 . . . . . . . . . 10 x, y {⟨x, x⟩, ⟨x, y⟩}
36 eleq2 2101 . . . . . . . . . 10 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → (⟨x, yu, 𝑡⟩ ↔ ⟨x, y {⟨x, x⟩, ⟨x, y⟩}))
3735, 36mpbiri 157 . . . . . . . . 9 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → ⟨x, yu, 𝑡⟩)
3833, 37jca 290 . . . . . . . 8 (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → (⟨x, xu, 𝑡x, yu, 𝑡⟩))
39 opeq12 3545 . . . . . . . . . . . . . 14 ((z = x w = x) → ⟨z, w⟩ = ⟨x, x⟩)
40393adant3 924 . . . . . . . . . . . . 13 ((z = x w = x v = y) → ⟨z, w⟩ = ⟨x, x⟩)
4140eleq1d 2106 . . . . . . . . . . . 12 ((z = x w = x v = y) → (⟨z, wu, 𝑡⟩ ↔ ⟨x, xu, 𝑡⟩))
42 opeq12 3545 . . . . . . . . . . . . . 14 ((z = x v = y) → ⟨z, v⟩ = ⟨x, y⟩)
43423adant2 923 . . . . . . . . . . . . 13 ((z = x w = x v = y) → ⟨z, v⟩ = ⟨x, y⟩)
4443eleq1d 2106 . . . . . . . . . . . 12 ((z = x w = x v = y) → (⟨z, vu, 𝑡⟩ ↔ ⟨x, yu, 𝑡⟩))
4541, 44anbi12d 442 . . . . . . . . . . 11 ((z = x w = x v = y) → ((⟨z, wu, 𝑡z, vu, 𝑡⟩) ↔ (⟨x, xu, 𝑡x, yu, 𝑡⟩)))
46 eqeq12 2052 . . . . . . . . . . . 12 ((w = x v = y) → (w = vx = y))
47463adant1 922 . . . . . . . . . . 11 ((z = x w = x v = y) → (w = vx = y))
4845, 47imbi12d 223 . . . . . . . . . 10 ((z = x w = x v = y) → (((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v) ↔ ((⟨x, xu, 𝑡x, yu, 𝑡⟩) → x = y)))
4948spc3gv 2642 . . . . . . . . 9 ((x V x V y V) → (zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v) → ((⟨x, xu, 𝑡x, yu, 𝑡⟩) → x = y)))
5015, 15, 18, 49mp3an 1232 . . . . . . . 8 (zwv((⟨z, wu, 𝑡z, vu, 𝑡⟩) → w = v) → ((⟨x, xu, 𝑡x, yu, 𝑡⟩) → x = y))
5129, 38, 50syl2im 34 . . . . . . 7 (Fun ⟨u, 𝑡⟩ → (⟨u, 𝑡⟩ = {⟨x, x⟩, ⟨x, y⟩} → x = y))
5227, 51syl5bi 141 . . . . . 6 (Fun ⟨u, 𝑡⟩ → ((u = {x} 𝑡 = {x, y}) → x = y))
53 dfsn2 3384 . . . . . . . . . . 11 {x} = {x, x}
54 preq2 3442 . . . . . . . . . . 11 (x = y → {x, x} = {x, y})
5553, 54syl5req 2085 . . . . . . . . . 10 (x = y → {x, y} = {x})
5655eqeq2d 2051 . . . . . . . . 9 (x = y → (𝑡 = {x, y} ↔ 𝑡 = {x}))
57 eqtr3 2059 . . . . . . . . . 10 ((u = {x} 𝑡 = {x}) → u = 𝑡)
5857expcom 109 . . . . . . . . 9 (𝑡 = {x} → (u = {x} → u = 𝑡))
5956, 58syl6bi 152 . . . . . . . 8 (x = y → (𝑡 = {x, y} → (u = {x} → u = 𝑡)))
6059com13 74 . . . . . . 7 (u = {x} → (𝑡 = {x, y} → (x = yu = 𝑡)))
6160imp 115 . . . . . 6 ((u = {x} 𝑡 = {x, y}) → (x = yu = 𝑡))
6252, 61sylcom 25 . . . . 5 (Fun ⟨u, 𝑡⟩ → ((u = {x} 𝑡 = {x, y}) → u = 𝑡))
6362exlimdvv 1777 . . . 4 (Fun ⟨u, 𝑡⟩ → (xy(u = {x} 𝑡 = {x, y}) → u = 𝑡))
6413, 63mpd 13 . . 3 (Fun ⟨u, 𝑡⟩ → u = 𝑡)
654, 8, 64vtocl2g 2614 . 2 ((A 𝑉 B 𝑊) → (Fun ⟨A, B⟩ → A = B))
66653impia 1101 1 ((A 𝑉 B 𝑊 Fun ⟨A, B⟩) → A = B)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 885  wal 1241   = wceq 1243  wex 1381   wcel 1393  Vcvv 2554  {csn 3370  {cpr 3371  cop 3373  Rel wrel 4296  Fun wfun 4842
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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3869  ax-pow 3921  ax-pr 3938
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-v 2556  df-un 2919  df-in 2921  df-ss 2928  df-pw 3356  df-sn 3376  df-pr 3377  df-op 3379  df-br 3759  df-opab 3813  df-id 4024  df-xp 4297  df-rel 4298  df-cnv 4299  df-co 4300  df-fun 4850
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator