Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disjdsct Structured version   Visualization version   GIF version

Theorem disjdsct 31166
Description: A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv 6539) (Contributed by Thierry Arnoux, 28-Feb-2017.)
Hypotheses
Ref Expression
disjdsct.0 𝑥𝜑
disjdsct.1 𝑥𝐴
disjdsct.2 ((𝜑𝑥𝐴) → 𝐵 ∈ (𝑉 ∖ {∅}))
disjdsct.3 (𝜑Disj 𝑥𝐴 𝐵)
Assertion
Ref Expression
disjdsct (𝜑 → Fun (𝑥𝐴𝐵))
Distinct variable group:   𝑥,𝑉
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem disjdsct
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 disjdsct.3 . . . . . . . 8 (𝜑Disj 𝑥𝐴 𝐵)
2 disjdsct.1 . . . . . . . . 9 𝑥𝐴
32disjorsf 31050 . . . . . . . 8 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
41, 3sylib 217 . . . . . . 7 (𝜑 → ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
54r19.21bi 3230 . . . . . 6 ((𝜑𝑖𝐴) → ∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
65r19.21bi 3230 . . . . 5 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
7 simpr3 1195 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐴𝑗𝐴 ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)
8 disjdsct.2 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝐵 ∈ (𝑉 ∖ {∅}))
9 eldifsni 4734 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅)
108, 9syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐵 ≠ ∅)
1110sbimi 2076 . . . . . . . . . . 11 ([𝑖 / 𝑥](𝜑𝑥𝐴) → [𝑖 / 𝑥]𝐵 ≠ ∅)
12 sban 2082 . . . . . . . . . . . 12 ([𝑖 / 𝑥](𝜑𝑥𝐴) ↔ ([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥𝐴))
13 disjdsct.0 . . . . . . . . . . . . . 14 𝑥𝜑
1413sbf 2262 . . . . . . . . . . . . 13 ([𝑖 / 𝑥]𝜑𝜑)
152clelsb1fw 2908 . . . . . . . . . . . . 13 ([𝑖 / 𝑥]𝑥𝐴𝑖𝐴)
1614, 15anbi12i 627 . . . . . . . . . . . 12 (([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥𝐴) ↔ (𝜑𝑖𝐴))
1712, 16bitri 274 . . . . . . . . . . 11 ([𝑖 / 𝑥](𝜑𝑥𝐴) ↔ (𝜑𝑖𝐴))
18 sbsbc 3729 . . . . . . . . . . . 12 ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ [𝑖 / 𝑥]𝐵 ≠ ∅)
19 sbcne12 4356 . . . . . . . . . . . 12 ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ 𝑖 / 𝑥𝐵𝑖 / 𝑥∅)
20 csb0 4351 . . . . . . . . . . . . 13 𝑖 / 𝑥∅ = ∅
2120neeq2i 3006 . . . . . . . . . . . 12 (𝑖 / 𝑥𝐵𝑖 / 𝑥∅ ↔ 𝑖 / 𝑥𝐵 ≠ ∅)
2218, 19, 213bitri 296 . . . . . . . . . . 11 ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ 𝑖 / 𝑥𝐵 ≠ ∅)
2311, 17, 223imtr3i 290 . . . . . . . . . 10 ((𝜑𝑖𝐴) → 𝑖 / 𝑥𝐵 ≠ ∅)
24233ad2antr1 1187 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐴𝑗𝐴 ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) → 𝑖 / 𝑥𝐵 ≠ ∅)
25 disj3 4397 . . . . . . . . . . . . 13 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ 𝑖 / 𝑥𝐵 = (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
2625biimpi 215 . . . . . . . . . . . 12 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → 𝑖 / 𝑥𝐵 = (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
2726neeq1d 3000 . . . . . . . . . . 11 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → (𝑖 / 𝑥𝐵 ≠ ∅ ↔ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) ≠ ∅))
2827biimpa 477 . . . . . . . . . 10 (((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∧ 𝑖 / 𝑥𝐵 ≠ ∅) → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) ≠ ∅)
29 difn0 4308 . . . . . . . . . 10 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) ≠ ∅ → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
3028, 29syl 17 . . . . . . . . 9 (((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∧ 𝑖 / 𝑥𝐵 ≠ ∅) → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
317, 24, 30syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑖𝐴𝑗𝐴 ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
32313anassrs 1359 . . . . . . 7 ((((𝜑𝑖𝐴) ∧ 𝑗𝐴) ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
3332ex 413 . . . . . 6 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
3433orim2d 964 . . . . 5 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)))
356, 34mpd 15 . . . 4 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
3635ralrimiva 3139 . . 3 ((𝜑𝑖𝐴) → ∀𝑗𝐴 (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
3736ralrimiva 3139 . 2 (𝜑 → ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
38 nfmpt1 5194 . . 3 𝑥(𝑥𝐴𝐵)
39 eqid 2736 . . 3 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
4013, 2, 38, 39, 8funcnv4mpt 31137 . 2 (𝜑 → (Fun (𝑥𝐴𝐵) ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)))
4137, 40mpbird 256 1 (𝜑 → Fun (𝑥𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 844  w3a 1086   = wceq 1540  wnf 1784  [wsb 2066  wcel 2105  wnfc 2884  wne 2940  wral 3061  [wsbc 3725  csb 3841  cdif 3893  cin 3895  c0 4266  {csn 4570  Disj wdisj 5051  cmpt 5169  ccnv 5606  Fun wfun 6459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-disj 5052  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-fv 6473
This theorem is referenced by:  esumrnmpt  32156  measvunilem  32316
  Copyright terms: Public domain W3C validator