MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fliftfun Structured version   Visualization version   GIF version

Theorem fliftfun 7257
Description: The function 𝐹 is the unique function defined by 𝐹𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
Hypotheses
Ref Expression
flift.1 𝐹 = ran (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
flift.2 ((𝜑𝑥𝑋) → 𝐴𝑅)
flift.3 ((𝜑𝑥𝑋) → 𝐵𝑆)
fliftfun.4 (𝑥 = 𝑦𝐴 = 𝐶)
fliftfun.5 (𝑥 = 𝑦𝐵 = 𝐷)
Assertion
Ref Expression
fliftfun (𝜑 → (Fun 𝐹 ↔ ∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷)))
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝑦,𝑅   𝑥,𝐷   𝑦,𝐹   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑦)   𝐷(𝑦)   𝐹(𝑥)

Proof of Theorem fliftfun
Dummy variables 𝑣 𝑢 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1917 . . 3 𝑥𝜑
2 flift.1 . . . . 5 𝐹 = ran (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
3 nfmpt1 5213 . . . . . 6 𝑥(𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
43nfrn 5907 . . . . 5 𝑥ran (𝑥𝑋 ↦ ⟨𝐴, 𝐵⟩)
52, 4nfcxfr 2905 . . . 4 𝑥𝐹
65nffun 6524 . . 3 𝑥Fun 𝐹
7 fveq2 6842 . . . . . . 7 (𝐴 = 𝐶 → (𝐹𝐴) = (𝐹𝐶))
8 simplr 767 . . . . . . . . 9 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → Fun 𝐹)
9 flift.2 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → 𝐴𝑅)
10 flift.3 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → 𝐵𝑆)
112, 9, 10fliftel1 7255 . . . . . . . . . 10 ((𝜑𝑥𝑋) → 𝐴𝐹𝐵)
1211ad2ant2r 745 . . . . . . . . 9 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → 𝐴𝐹𝐵)
13 funbrfv 6893 . . . . . . . . 9 (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹𝐴) = 𝐵))
148, 12, 13sylc 65 . . . . . . . 8 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹𝐴) = 𝐵)
15 simprr 771 . . . . . . . . . . 11 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
16 eqidd 2737 . . . . . . . . . . 11 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → 𝐶 = 𝐶)
17 eqidd 2737 . . . . . . . . . . 11 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → 𝐷 = 𝐷)
18 fliftfun.4 . . . . . . . . . . . . . 14 (𝑥 = 𝑦𝐴 = 𝐶)
1918eqeq2d 2747 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐶 = 𝐴𝐶 = 𝐶))
20 fliftfun.5 . . . . . . . . . . . . . 14 (𝑥 = 𝑦𝐵 = 𝐷)
2120eqeq2d 2747 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐷 = 𝐵𝐷 = 𝐷))
2219, 21anbi12d 631 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐶 = 𝐴𝐷 = 𝐵) ↔ (𝐶 = 𝐶𝐷 = 𝐷)))
2322rspcev 3581 . . . . . . . . . . 11 ((𝑦𝑋 ∧ (𝐶 = 𝐶𝐷 = 𝐷)) → ∃𝑥𝑋 (𝐶 = 𝐴𝐷 = 𝐵))
2415, 16, 17, 23syl12anc 835 . . . . . . . . . 10 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → ∃𝑥𝑋 (𝐶 = 𝐴𝐷 = 𝐵))
252, 9, 10fliftel 7254 . . . . . . . . . . 11 (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥𝑋 (𝐶 = 𝐴𝐷 = 𝐵)))
2625ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → (𝐶𝐹𝐷 ↔ ∃𝑥𝑋 (𝐶 = 𝐴𝐷 = 𝐵)))
2724, 26mpbird 256 . . . . . . . . 9 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → 𝐶𝐹𝐷)
28 funbrfv 6893 . . . . . . . . 9 (Fun 𝐹 → (𝐶𝐹𝐷 → (𝐹𝐶) = 𝐷))
298, 27, 28sylc 65 . . . . . . . 8 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → (𝐹𝐶) = 𝐷)
3014, 29eqeq12d 2752 . . . . . . 7 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → ((𝐹𝐴) = (𝐹𝐶) ↔ 𝐵 = 𝐷))
317, 30imbitrid 243 . . . . . 6 (((𝜑 ∧ Fun 𝐹) ∧ (𝑥𝑋𝑦𝑋)) → (𝐴 = 𝐶𝐵 = 𝐷))
3231anassrs 468 . . . . 5 ((((𝜑 ∧ Fun 𝐹) ∧ 𝑥𝑋) ∧ 𝑦𝑋) → (𝐴 = 𝐶𝐵 = 𝐷))
3332ralrimiva 3143 . . . 4 (((𝜑 ∧ Fun 𝐹) ∧ 𝑥𝑋) → ∀𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷))
3433exp31 420 . . 3 (𝜑 → (Fun 𝐹 → (𝑥𝑋 → ∀𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷))))
351, 6, 34ralrimd 3247 . 2 (𝜑 → (Fun 𝐹 → ∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷)))
362, 9, 10fliftel 7254 . . . . . . . . 9 (𝜑 → (𝑧𝐹𝑢 ↔ ∃𝑥𝑋 (𝑧 = 𝐴𝑢 = 𝐵)))
372, 9, 10fliftel 7254 . . . . . . . . . 10 (𝜑 → (𝑧𝐹𝑣 ↔ ∃𝑥𝑋 (𝑧 = 𝐴𝑣 = 𝐵)))
3818eqeq2d 2747 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑧 = 𝐴𝑧 = 𝐶))
3920eqeq2d 2747 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑣 = 𝐵𝑣 = 𝐷))
4038, 39anbi12d 631 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑣 = 𝐵) ↔ (𝑧 = 𝐶𝑣 = 𝐷)))
4140cbvrexvw 3226 . . . . . . . . . 10 (∃𝑥𝑋 (𝑧 = 𝐴𝑣 = 𝐵) ↔ ∃𝑦𝑋 (𝑧 = 𝐶𝑣 = 𝐷))
4237, 41bitrdi 286 . . . . . . . . 9 (𝜑 → (𝑧𝐹𝑣 ↔ ∃𝑦𝑋 (𝑧 = 𝐶𝑣 = 𝐷)))
4336, 42anbi12d 631 . . . . . . . 8 (𝜑 → ((𝑧𝐹𝑢𝑧𝐹𝑣) ↔ (∃𝑥𝑋 (𝑧 = 𝐴𝑢 = 𝐵) ∧ ∃𝑦𝑋 (𝑧 = 𝐶𝑣 = 𝐷))))
4443biimpd 228 . . . . . . 7 (𝜑 → ((𝑧𝐹𝑢𝑧𝐹𝑣) → (∃𝑥𝑋 (𝑧 = 𝐴𝑢 = 𝐵) ∧ ∃𝑦𝑋 (𝑧 = 𝐶𝑣 = 𝐷))))
45 reeanv 3217 . . . . . . . 8 (∃𝑥𝑋𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷)) ↔ (∃𝑥𝑋 (𝑧 = 𝐴𝑢 = 𝐵) ∧ ∃𝑦𝑋 (𝑧 = 𝐶𝑣 = 𝐷)))
46 r19.29 3117 . . . . . . . . . 10 ((∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → ∃𝑥𝑋 (∀𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) ∧ ∃𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))))
47 r19.29 3117 . . . . . . . . . . . 12 ((∀𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) ∧ ∃𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → ∃𝑦𝑋 ((𝐴 = 𝐶𝐵 = 𝐷) ∧ ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))))
48 eqtr2 2760 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝐴𝑧 = 𝐶) → 𝐴 = 𝐶)
4948ad2ant2r 745 . . . . . . . . . . . . . . . 16 (((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷)) → 𝐴 = 𝐶)
5049imim1i 63 . . . . . . . . . . . . . . 15 ((𝐴 = 𝐶𝐵 = 𝐷) → (((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷)) → 𝐵 = 𝐷))
5150imp 407 . . . . . . . . . . . . . 14 (((𝐴 = 𝐶𝐵 = 𝐷) ∧ ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝐵 = 𝐷)
52 simprlr 778 . . . . . . . . . . . . . 14 (((𝐴 = 𝐶𝐵 = 𝐷) ∧ ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝑢 = 𝐵)
53 simprrr 780 . . . . . . . . . . . . . 14 (((𝐴 = 𝐶𝐵 = 𝐷) ∧ ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝑣 = 𝐷)
5451, 52, 533eqtr4d 2786 . . . . . . . . . . . . 13 (((𝐴 = 𝐶𝐵 = 𝐷) ∧ ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝑢 = 𝑣)
5554rexlimivw 3148 . . . . . . . . . . . 12 (∃𝑦𝑋 ((𝐴 = 𝐶𝐵 = 𝐷) ∧ ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝑢 = 𝑣)
5647, 55syl 17 . . . . . . . . . . 11 ((∀𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) ∧ ∃𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝑢 = 𝑣)
5756rexlimivw 3148 . . . . . . . . . 10 (∃𝑥𝑋 (∀𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) ∧ ∃𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝑢 = 𝑣)
5846, 57syl 17 . . . . . . . . 9 ((∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) ∧ ∃𝑥𝑋𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷))) → 𝑢 = 𝑣)
5958ex 413 . . . . . . . 8 (∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) → (∃𝑥𝑋𝑦𝑋 ((𝑧 = 𝐴𝑢 = 𝐵) ∧ (𝑧 = 𝐶𝑣 = 𝐷)) → 𝑢 = 𝑣))
6045, 59biimtrrid 242 . . . . . . 7 (∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) → ((∃𝑥𝑋 (𝑧 = 𝐴𝑢 = 𝐵) ∧ ∃𝑦𝑋 (𝑧 = 𝐶𝑣 = 𝐷)) → 𝑢 = 𝑣))
6144, 60syl9 77 . . . . . 6 (𝜑 → (∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) → ((𝑧𝐹𝑢𝑧𝐹𝑣) → 𝑢 = 𝑣)))
6261alrimdv 1932 . . . . 5 (𝜑 → (∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) → ∀𝑣((𝑧𝐹𝑢𝑧𝐹𝑣) → 𝑢 = 𝑣)))
6362alrimdv 1932 . . . 4 (𝜑 → (∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) → ∀𝑢𝑣((𝑧𝐹𝑢𝑧𝐹𝑣) → 𝑢 = 𝑣)))
6463alrimdv 1932 . . 3 (𝜑 → (∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) → ∀𝑧𝑢𝑣((𝑧𝐹𝑢𝑧𝐹𝑣) → 𝑢 = 𝑣)))
652, 9, 10fliftrel 7253 . . . . 5 (𝜑𝐹 ⊆ (𝑅 × 𝑆))
66 relxp 5651 . . . . 5 Rel (𝑅 × 𝑆)
67 relss 5737 . . . . 5 (𝐹 ⊆ (𝑅 × 𝑆) → (Rel (𝑅 × 𝑆) → Rel 𝐹))
6865, 66, 67mpisyl 21 . . . 4 (𝜑 → Rel 𝐹)
69 dffun2 6506 . . . . 5 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑧𝑢𝑣((𝑧𝐹𝑢𝑧𝐹𝑣) → 𝑢 = 𝑣)))
7069baib 536 . . . 4 (Rel 𝐹 → (Fun 𝐹 ↔ ∀𝑧𝑢𝑣((𝑧𝐹𝑢𝑧𝐹𝑣) → 𝑢 = 𝑣)))
7168, 70syl 17 . . 3 (𝜑 → (Fun 𝐹 ↔ ∀𝑧𝑢𝑣((𝑧𝐹𝑢𝑧𝐹𝑣) → 𝑢 = 𝑣)))
7264, 71sylibrd 258 . 2 (𝜑 → (∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷) → Fun 𝐹))
7335, 72impbid 211 1 (𝜑 → (Fun 𝐹 ↔ ∀𝑥𝑋𝑦𝑋 (𝐴 = 𝐶𝐵 = 𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1539   = wceq 1541  wcel 2106  wral 3064  wrex 3073  wss 3910  cop 4592   class class class wbr 5105  cmpt 5188   × cxp 5631  ran crn 5634  Rel wrel 5638  Fun wfun 6490  cfv 6496
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504
This theorem is referenced by:  fliftfund  7258  fliftfuns  7259  qliftfun  8741
  Copyright terms: Public domain W3C validator