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

Theorem ixpsnf1o 8234
 Description: A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
Hypothesis
Ref Expression
ixpsnf1o.f 𝐹 = (𝑥𝐴 ↦ ({𝐼} × {𝑥}))
Assertion
Ref Expression
ixpsnf1o (𝐼𝑉𝐹:𝐴1-1-ontoX𝑦 ∈ {𝐼}𝐴)
Distinct variable groups:   𝑥,𝐼,𝑦   𝑥,𝐴,𝑦   𝑥,𝑉,𝑦   𝑦,𝐹
Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem ixpsnf1o
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ixpsnf1o.f . 2 𝐹 = (𝑥𝐴 ↦ ({𝐼} × {𝑥}))
2 snex 5140 . . . 4 {𝐼} ∈ V
3 snex 5140 . . . 4 {𝑥} ∈ V
42, 3xpex 7240 . . 3 ({𝐼} × {𝑥}) ∈ V
54a1i 11 . 2 ((𝐼𝑉𝑥𝐴) → ({𝐼} × {𝑥}) ∈ V)
6 vex 3400 . . . . 5 𝑎 ∈ V
76rnex 7379 . . . 4 ran 𝑎 ∈ V
87uniex 7230 . . 3 ran 𝑎 ∈ V
98a1i 11 . 2 ((𝐼𝑉𝑎X𝑦 ∈ {𝐼}𝐴) → ran 𝑎 ∈ V)
10 sneq 4407 . . . . . 6 (𝑏 = 𝐼 → {𝑏} = {𝐼})
1110xpeq1d 5384 . . . . 5 (𝑏 = 𝐼 → ({𝑏} × {𝑥}) = ({𝐼} × {𝑥}))
1211eqeq2d 2787 . . . 4 (𝑏 = 𝐼 → (𝑎 = ({𝑏} × {𝑥}) ↔ 𝑎 = ({𝐼} × {𝑥})))
1312anbi2d 622 . . 3 (𝑏 = 𝐼 → ((𝑥𝐴𝑎 = ({𝑏} × {𝑥})) ↔ (𝑥𝐴𝑎 = ({𝐼} × {𝑥}))))
14 elixpsn 8233 . . . . . 6 (𝑏 ∈ V → (𝑎X𝑦 ∈ {𝑏}𝐴 ↔ ∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩}))
1514elv 3401 . . . . 5 (𝑎X𝑦 ∈ {𝑏}𝐴 ↔ ∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩})
1610ixpeq1d 8206 . . . . . 6 (𝑏 = 𝐼X𝑦 ∈ {𝑏}𝐴 = X𝑦 ∈ {𝐼}𝐴)
1716eleq2d 2844 . . . . 5 (𝑏 = 𝐼 → (𝑎X𝑦 ∈ {𝑏}𝐴𝑎X𝑦 ∈ {𝐼}𝐴))
1815, 17syl5bbr 277 . . . 4 (𝑏 = 𝐼 → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ↔ 𝑎X𝑦 ∈ {𝐼}𝐴))
1918anbi1d 623 . . 3 (𝑏 = 𝐼 → ((∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎) ↔ (𝑎X𝑦 ∈ {𝐼}𝐴𝑥 = ran 𝑎)))
20 vex 3400 . . . . . . 7 𝑏 ∈ V
21 vex 3400 . . . . . . 7 𝑥 ∈ V
2220, 21xpsn 6672 . . . . . 6 ({𝑏} × {𝑥}) = {⟨𝑏, 𝑥⟩}
2322eqeq2i 2789 . . . . 5 (𝑎 = ({𝑏} × {𝑥}) ↔ 𝑎 = {⟨𝑏, 𝑥⟩})
2423anbi2i 616 . . . 4 ((𝑥𝐴𝑎 = ({𝑏} × {𝑥})) ↔ (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}))
25 eqid 2777 . . . . . . . . 9 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑥⟩}
26 opeq2 4637 . . . . . . . . . . 11 (𝑐 = 𝑥 → ⟨𝑏, 𝑐⟩ = ⟨𝑏, 𝑥⟩)
2726sneqd 4409 . . . . . . . . . 10 (𝑐 = 𝑥 → {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})
2827rspceeqv 3528 . . . . . . . . 9 ((𝑥𝐴 ∧ {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑥⟩}) → ∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩})
2925, 28mpan2 681 . . . . . . . 8 (𝑥𝐴 → ∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩})
3020, 21op2nda 5875 . . . . . . . . 9 ran {⟨𝑏, 𝑥⟩} = 𝑥
3130eqcomi 2786 . . . . . . . 8 𝑥 = ran {⟨𝑏, 𝑥⟩}
3229, 31jctir 516 . . . . . . 7 (𝑥𝐴 → (∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran {⟨𝑏, 𝑥⟩}))
33 eqeq1 2781 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑥⟩} → (𝑎 = {⟨𝑏, 𝑐⟩} ↔ {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩}))
3433rexbidv 3236 . . . . . . . 8 (𝑎 = {⟨𝑏, 𝑥⟩} → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ↔ ∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩}))
35 rneq 5596 . . . . . . . . . 10 (𝑎 = {⟨𝑏, 𝑥⟩} → ran 𝑎 = ran {⟨𝑏, 𝑥⟩})
3635unieqd 4681 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑥⟩} → ran 𝑎 = ran {⟨𝑏, 𝑥⟩})
3736eqeq2d 2787 . . . . . . . 8 (𝑎 = {⟨𝑏, 𝑥⟩} → (𝑥 = ran 𝑎𝑥 = ran {⟨𝑏, 𝑥⟩}))
3834, 37anbi12d 624 . . . . . . 7 (𝑎 = {⟨𝑏, 𝑥⟩} → ((∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎) ↔ (∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran {⟨𝑏, 𝑥⟩})))
3932, 38syl5ibrcom 239 . . . . . 6 (𝑥𝐴 → (𝑎 = {⟨𝑏, 𝑥⟩} → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎)))
4039imp 397 . . . . 5 ((𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}) → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎))
41 vex 3400 . . . . . . . . . . 11 𝑐 ∈ V
4220, 41op2nda 5875 . . . . . . . . . 10 ran {⟨𝑏, 𝑐⟩} = 𝑐
4342eqeq2i 2789 . . . . . . . . 9 (𝑥 = ran {⟨𝑏, 𝑐⟩} ↔ 𝑥 = 𝑐)
44 eqidd 2778 . . . . . . . . . . 11 (𝑐𝐴 → {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩})
4544ancli 544 . . . . . . . . . 10 (𝑐𝐴 → (𝑐𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩}))
46 eleq1w 2841 . . . . . . . . . . 11 (𝑥 = 𝑐 → (𝑥𝐴𝑐𝐴))
47 opeq2 4637 . . . . . . . . . . . . 13 (𝑥 = 𝑐 → ⟨𝑏, 𝑥⟩ = ⟨𝑏, 𝑐⟩)
4847sneqd 4409 . . . . . . . . . . . 12 (𝑥 = 𝑐 → {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩})
4948eqeq2d 2787 . . . . . . . . . . 11 (𝑥 = 𝑐 → ({⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩} ↔ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩}))
5046, 49anbi12d 624 . . . . . . . . . 10 (𝑥 = 𝑐 → ((𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩}) ↔ (𝑐𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩})))
5145, 50syl5ibrcom 239 . . . . . . . . 9 (𝑐𝐴 → (𝑥 = 𝑐 → (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})))
5243, 51syl5bi 234 . . . . . . . 8 (𝑐𝐴 → (𝑥 = ran {⟨𝑏, 𝑐⟩} → (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})))
53 rneq 5596 . . . . . . . . . . 11 (𝑎 = {⟨𝑏, 𝑐⟩} → ran 𝑎 = ran {⟨𝑏, 𝑐⟩})
5453unieqd 4681 . . . . . . . . . 10 (𝑎 = {⟨𝑏, 𝑐⟩} → ran 𝑎 = ran {⟨𝑏, 𝑐⟩})
5554eqeq2d 2787 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑐⟩} → (𝑥 = ran 𝑎𝑥 = ran {⟨𝑏, 𝑐⟩}))
56 eqeq1 2781 . . . . . . . . . 10 (𝑎 = {⟨𝑏, 𝑐⟩} → (𝑎 = {⟨𝑏, 𝑥⟩} ↔ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩}))
5756anbi2d 622 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑐⟩} → ((𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}) ↔ (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})))
5855, 57imbi12d 336 . . . . . . . 8 (𝑎 = {⟨𝑏, 𝑐⟩} → ((𝑥 = ran 𝑎 → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩})) ↔ (𝑥 = ran {⟨𝑏, 𝑐⟩} → (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩}))))
5952, 58syl5ibrcom 239 . . . . . . 7 (𝑐𝐴 → (𝑎 = {⟨𝑏, 𝑐⟩} → (𝑥 = ran 𝑎 → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}))))
6059rexlimiv 3208 . . . . . 6 (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} → (𝑥 = ran 𝑎 → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩})))
6160imp 397 . . . . 5 ((∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎) → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}))
6240, 61impbii 201 . . . 4 ((𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}) ↔ (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎))
6324, 62bitri 267 . . 3 ((𝑥𝐴𝑎 = ({𝑏} × {𝑥})) ↔ (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎))
6413, 19, 63vtoclbg 3467 . 2 (𝐼𝑉 → ((𝑥𝐴𝑎 = ({𝐼} × {𝑥})) ↔ (𝑎X𝑦 ∈ {𝐼}𝐴𝑥 = ran 𝑎)))
651, 5, 9, 64f1od 7162 1 (𝐼𝑉𝐹:𝐴1-1-ontoX𝑦 ∈ {𝐼}𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2106  ∃wrex 3090  Vcvv 3397  {csn 4397  ⟨cop 4403  ∪ cuni 4671   ↦ cmpt 4965   × cxp 5353  ran crn 5356  –1-1-onto→wf1o 6134  Xcixp 8194 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ixp 8195 This theorem is referenced by:  mapsnf1o  8235
 Copyright terms: Public domain W3C validator