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

Theorem funtpg 4876
Description: A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017.)
Assertion
Ref Expression
funtpg (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → Fun {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩})

Proof of Theorem funtpg
StepHypRef Expression
1 3simpa 889 . . . 4 ((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) → (𝑋 𝑈 𝑌 𝑉))
2 3simpa 889 . . . 4 ((A 𝐹 B 𝐺 𝐶 𝐻) → (A 𝐹 B 𝐺))
3 simp1 892 . . . 4 ((𝑋𝑌 𝑋𝑍 𝑌𝑍) → 𝑋𝑌)
4 funprg 4875 . . . 4 (((𝑋 𝑈 𝑌 𝑉) (A 𝐹 B 𝐺) 𝑋𝑌) → Fun {⟨𝑋, A⟩, ⟨𝑌, B⟩})
51, 2, 3, 4syl3an 1163 . . 3 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → Fun {⟨𝑋, A⟩, ⟨𝑌, B⟩})
6 simp13 924 . . . 4 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → 𝑍 𝑊)
7 simp23 927 . . . 4 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → 𝐶 𝐻)
8 funsng 4872 . . . 4 ((𝑍 𝑊 𝐶 𝐻) → Fun {⟨𝑍, 𝐶⟩})
96, 7, 8syl2anc 393 . . 3 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → Fun {⟨𝑍, 𝐶⟩})
1023ad2ant2 914 . . . . . 6 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → (A 𝐹 B 𝐺))
11 dmpropg 4720 . . . . . 6 ((A 𝐹 B 𝐺) → dom {⟨𝑋, A⟩, ⟨𝑌, B⟩} = {𝑋, 𝑌})
1210, 11syl 14 . . . . 5 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → dom {⟨𝑋, A⟩, ⟨𝑌, B⟩} = {𝑋, 𝑌})
13 dmsnopg 4719 . . . . . 6 (𝐶 𝐻 → dom {⟨𝑍, 𝐶⟩} = {𝑍})
147, 13syl 14 . . . . 5 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → dom {⟨𝑍, 𝐶⟩} = {𝑍})
1512, 14ineq12d 3116 . . . 4 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → (dom {⟨𝑋, A⟩, ⟨𝑌, B⟩} ∩ dom {⟨𝑍, 𝐶⟩}) = ({𝑋, 𝑌} ∩ {𝑍}))
16 elpri 3370 . . . . . . . 8 (𝑍 {𝑋, 𝑌} → (𝑍 = 𝑋 𝑍 = 𝑌))
17 nner 2192 . . . . . . . . . . . 12 (𝑋 = 𝑍 → ¬ 𝑋𝑍)
1817eqcoms 2025 . . . . . . . . . . 11 (𝑍 = 𝑋 → ¬ 𝑋𝑍)
19 3mix2 1062 . . . . . . . . . . 11 𝑋𝑍 → (¬ 𝑋𝑌 ¬ 𝑋𝑍 ¬ 𝑌𝑍))
2018, 19syl 14 . . . . . . . . . 10 (𝑍 = 𝑋 → (¬ 𝑋𝑌 ¬ 𝑋𝑍 ¬ 𝑌𝑍))
21 nner 2192 . . . . . . . . . . . 12 (𝑌 = 𝑍 → ¬ 𝑌𝑍)
2221eqcoms 2025 . . . . . . . . . . 11 (𝑍 = 𝑌 → ¬ 𝑌𝑍)
23 3mix3 1063 . . . . . . . . . . 11 𝑌𝑍 → (¬ 𝑋𝑌 ¬ 𝑋𝑍 ¬ 𝑌𝑍))
2422, 23syl 14 . . . . . . . . . 10 (𝑍 = 𝑌 → (¬ 𝑋𝑌 ¬ 𝑋𝑍 ¬ 𝑌𝑍))
2520, 24jaoi 623 . . . . . . . . 9 ((𝑍 = 𝑋 𝑍 = 𝑌) → (¬ 𝑋𝑌 ¬ 𝑋𝑍 ¬ 𝑌𝑍))
26 3ianorr 1189 . . . . . . . . 9 ((¬ 𝑋𝑌 ¬ 𝑋𝑍 ¬ 𝑌𝑍) → ¬ (𝑋𝑌 𝑋𝑍 𝑌𝑍))
2725, 26syl 14 . . . . . . . 8 ((𝑍 = 𝑋 𝑍 = 𝑌) → ¬ (𝑋𝑌 𝑋𝑍 𝑌𝑍))
2816, 27syl 14 . . . . . . 7 (𝑍 {𝑋, 𝑌} → ¬ (𝑋𝑌 𝑋𝑍 𝑌𝑍))
2928con2i 545 . . . . . 6 ((𝑋𝑌 𝑋𝑍 𝑌𝑍) → ¬ 𝑍 {𝑋, 𝑌})
30 disjsn 3406 . . . . . 6 (({𝑋, 𝑌} ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 {𝑋, 𝑌})
3129, 30sylibr 137 . . . . 5 ((𝑋𝑌 𝑋𝑍 𝑌𝑍) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅)
32313ad2ant3 915 . . . 4 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅)
3315, 32eqtrd 2054 . . 3 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → (dom {⟨𝑋, A⟩, ⟨𝑌, B⟩} ∩ dom {⟨𝑍, 𝐶⟩}) = ∅)
34 funun 4870 . . 3 (((Fun {⟨𝑋, A⟩, ⟨𝑌, B⟩} Fun {⟨𝑍, 𝐶⟩}) (dom {⟨𝑋, A⟩, ⟨𝑌, B⟩} ∩ dom {⟨𝑍, 𝐶⟩}) = ∅) → Fun ({⟨𝑋, A⟩, ⟨𝑌, B⟩} ∪ {⟨𝑍, 𝐶⟩}))
355, 9, 33, 34syl21anc 1120 . 2 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → Fun ({⟨𝑋, A⟩, ⟨𝑌, B⟩} ∪ {⟨𝑍, 𝐶⟩}))
36 df-tp 3358 . . 3 {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩} = ({⟨𝑋, A⟩, ⟨𝑌, B⟩} ∪ {⟨𝑍, 𝐶⟩})
3736funeqi 4848 . 2 (Fun {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩} ↔ Fun ({⟨𝑋, A⟩, ⟨𝑌, B⟩} ∪ {⟨𝑍, 𝐶⟩}))
3835, 37sylibr 137 1 (((𝑋 𝑈 𝑌 𝑉 𝑍 𝑊) (A 𝐹 B 𝐺 𝐶 𝐻) (𝑋𝑌 𝑋𝑍 𝑌𝑍)) → Fun {⟨𝑋, A⟩, ⟨𝑌, B⟩, ⟨𝑍, 𝐶⟩})
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97   wo 616   w3o 872   w3a 873   = wceq 1228   wcel 1374  wne 2186  cun 2892  cin 2893  c0 3201  {csn 3350  {cpr 3351  {ctp 3352  cop 3353  dom cdm 4272  Fun wfun 4823
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-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918
This theorem depends on definitions:  df-bi 110  df-3or 874  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-v 2537  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-tp 3358  df-op 3359  df-br 3739  df-opab 3793  df-id 4004  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-fun 4831
This theorem is referenced by:  fntpg  4881
  Copyright terms: Public domain W3C validator