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

Theorem disjdsct 30465
 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 6397) (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 30346 . . . . . . . 8 (Disj 𝑥𝐴 𝐵 ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
41, 3sylib 221 . . . . . . 7 (𝜑 → ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
54r19.21bi 3176 . . . . . 6 ((𝜑𝑖𝐴) → ∀𝑗𝐴 (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
65r19.21bi 3176 . . . . 5 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → (𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅))
7 simpr3 1193 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐴𝑗𝐴 ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)
8 disjdsct.2 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝐵 ∈ (𝑉 ∖ {∅}))
9 eldifsni 4686 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑉 ∖ {∅}) → 𝐵 ≠ ∅)
108, 9syl 17 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → 𝐵 ≠ ∅)
1110sbimi 2079 . . . . . . . . . . 11 ([𝑖 / 𝑥](𝜑𝑥𝐴) → [𝑖 / 𝑥]𝐵 ≠ ∅)
12 sban 2085 . . . . . . . . . . . 12 ([𝑖 / 𝑥](𝜑𝑥𝐴) ↔ ([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥𝐴))
13 disjdsct.0 . . . . . . . . . . . . . 14 𝑥𝜑
1413sbf 2270 . . . . . . . . . . . . 13 ([𝑖 / 𝑥]𝜑𝜑)
152clelsb3fw 2962 . . . . . . . . . . . . 13 ([𝑖 / 𝑥]𝑥𝐴𝑖𝐴)
1614, 15anbi12i 629 . . . . . . . . . . . 12 (([𝑖 / 𝑥]𝜑 ∧ [𝑖 / 𝑥]𝑥𝐴) ↔ (𝜑𝑖𝐴))
1712, 16bitri 278 . . . . . . . . . . 11 ([𝑖 / 𝑥](𝜑𝑥𝐴) ↔ (𝜑𝑖𝐴))
18 sbsbc 3727 . . . . . . . . . . . 12 ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ [𝑖 / 𝑥]𝐵 ≠ ∅)
19 sbcne12 4323 . . . . . . . . . . . 12 ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ 𝑖 / 𝑥𝐵𝑖 / 𝑥∅)
20 csb0 4317 . . . . . . . . . . . . 13 𝑖 / 𝑥∅ = ∅
2120neeq2i 3055 . . . . . . . . . . . 12 (𝑖 / 𝑥𝐵𝑖 / 𝑥∅ ↔ 𝑖 / 𝑥𝐵 ≠ ∅)
2218, 19, 213bitri 300 . . . . . . . . . . 11 ([𝑖 / 𝑥]𝐵 ≠ ∅ ↔ 𝑖 / 𝑥𝐵 ≠ ∅)
2311, 17, 223imtr3i 294 . . . . . . . . . 10 ((𝜑𝑖𝐴) → 𝑖 / 𝑥𝐵 ≠ ∅)
24233ad2antr1 1185 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐴𝑗𝐴 ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) → 𝑖 / 𝑥𝐵 ≠ ∅)
25 disj3 4364 . . . . . . . . . . . . 13 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ↔ 𝑖 / 𝑥𝐵 = (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
2625biimpi 219 . . . . . . . . . . . 12 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → 𝑖 / 𝑥𝐵 = (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
2726neeq1d 3049 . . . . . . . . . . 11 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → (𝑖 / 𝑥𝐵 ≠ ∅ ↔ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) ≠ ∅))
2827biimpa 480 . . . . . . . . . 10 (((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∧ 𝑖 / 𝑥𝐵 ≠ ∅) → (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) ≠ ∅)
29 difn0 4281 . . . . . . . . . 10 ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) ≠ ∅ → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
3028, 29syl 17 . . . . . . . . 9 (((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ ∧ 𝑖 / 𝑥𝐵 ≠ ∅) → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
317, 24, 30syl2anc 587 . . . . . . . 8 ((𝜑 ∧ (𝑖𝐴𝑗𝐴 ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅)) → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
32313anassrs 1357 . . . . . . 7 ((((𝜑𝑖𝐴) ∧ 𝑗𝐴) ∧ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)
3332ex 416 . . . . . 6 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → ((𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅ → 𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
3433orim2d 964 . . . . 5 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → ((𝑖 = 𝑗 ∨ (𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵) = ∅) → (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)))
356, 34mpd 15 . . . 4 (((𝜑𝑖𝐴) ∧ 𝑗𝐴) → (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
3635ralrimiva 3152 . . 3 ((𝜑𝑖𝐴) → ∀𝑗𝐴 (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
3736ralrimiva 3152 . 2 (𝜑 → ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵))
38 nfmpt1 5131 . . 3 𝑥(𝑥𝐴𝐵)
39 eqid 2801 . . 3 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
4013, 2, 38, 39, 8funcnv4mpt 30435 . 2 (𝜑 → (Fun (𝑥𝐴𝐵) ↔ ∀𝑖𝐴𝑗𝐴 (𝑖 = 𝑗𝑖 / 𝑥𝐵𝑗 / 𝑥𝐵)))
4137, 40mpbird 260 1 (𝜑 → Fun (𝑥𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  Ⅎwnf 1785  [wsb 2069   ∈ wcel 2112  Ⅎwnfc 2939   ≠ wne 2990  ∀wral 3109  [wsbc 3723  ⦋csb 3831   ∖ cdif 3881   ∩ cin 3883  ∅c0 4246  {csn 4528  Disj wdisj 4998   ↦ cmpt 5113  ◡ccnv 5522  Fun wfun 6322 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-disj 4999  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-fv 6336 This theorem is referenced by:  esumrnmpt  31419  measvunilem  31579
 Copyright terms: Public domain W3C validator