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

Theorem ixpsnf1o 6730
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 snexg 4181 . . . 4 (𝐼𝑉 → {𝐼} ∈ V)
3 vex 2740 . . . . 5 𝑥 ∈ V
43snex 4182 . . . 4 {𝑥} ∈ V
5 xpexg 4737 . . . 4 (({𝐼} ∈ V ∧ {𝑥} ∈ V) → ({𝐼} × {𝑥}) ∈ V)
62, 4, 5sylancl 413 . . 3 (𝐼𝑉 → ({𝐼} × {𝑥}) ∈ V)
76adantr 276 . 2 ((𝐼𝑉𝑥𝐴) → ({𝐼} × {𝑥}) ∈ V)
8 vex 2740 . . . . 5 𝑎 ∈ V
98rnex 4890 . . . 4 ran 𝑎 ∈ V
109uniex 4434 . . 3 ran 𝑎 ∈ V
1110a1i 9 . 2 ((𝐼𝑉𝑎X𝑦 ∈ {𝐼}𝐴) → ran 𝑎 ∈ V)
12 sneq 3602 . . . . . 6 (𝑏 = 𝐼 → {𝑏} = {𝐼})
1312xpeq1d 4646 . . . . 5 (𝑏 = 𝐼 → ({𝑏} × {𝑥}) = ({𝐼} × {𝑥}))
1413eqeq2d 2189 . . . 4 (𝑏 = 𝐼 → (𝑎 = ({𝑏} × {𝑥}) ↔ 𝑎 = ({𝐼} × {𝑥})))
1514anbi2d 464 . . 3 (𝑏 = 𝐼 → ((𝑥𝐴𝑎 = ({𝑏} × {𝑥})) ↔ (𝑥𝐴𝑎 = ({𝐼} × {𝑥}))))
16 elixpsn 6729 . . . . . 6 (𝑏 ∈ V → (𝑎X𝑦 ∈ {𝑏}𝐴 ↔ ∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩}))
1716elv 2741 . . . . 5 (𝑎X𝑦 ∈ {𝑏}𝐴 ↔ ∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩})
1812ixpeq1d 6704 . . . . . 6 (𝑏 = 𝐼X𝑦 ∈ {𝑏}𝐴 = X𝑦 ∈ {𝐼}𝐴)
1918eleq2d 2247 . . . . 5 (𝑏 = 𝐼 → (𝑎X𝑦 ∈ {𝑏}𝐴𝑎X𝑦 ∈ {𝐼}𝐴))
2017, 19bitr3id 194 . . . 4 (𝑏 = 𝐼 → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ↔ 𝑎X𝑦 ∈ {𝐼}𝐴))
2120anbi1d 465 . . 3 (𝑏 = 𝐼 → ((∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎) ↔ (𝑎X𝑦 ∈ {𝐼}𝐴𝑥 = ran 𝑎)))
22 vex 2740 . . . . . . 7 𝑏 ∈ V
2322, 3xpsn 5688 . . . . . 6 ({𝑏} × {𝑥}) = {⟨𝑏, 𝑥⟩}
2423eqeq2i 2188 . . . . 5 (𝑎 = ({𝑏} × {𝑥}) ↔ 𝑎 = {⟨𝑏, 𝑥⟩})
2524anbi2i 457 . . . 4 ((𝑥𝐴𝑎 = ({𝑏} × {𝑥})) ↔ (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}))
26 eqid 2177 . . . . . . . . 9 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑥⟩}
27 opeq2 3777 . . . . . . . . . . 11 (𝑐 = 𝑥 → ⟨𝑏, 𝑐⟩ = ⟨𝑏, 𝑥⟩)
2827sneqd 3604 . . . . . . . . . 10 (𝑐 = 𝑥 → {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})
2928rspceeqv 2859 . . . . . . . . 9 ((𝑥𝐴 ∧ {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑥⟩}) → ∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩})
3026, 29mpan2 425 . . . . . . . 8 (𝑥𝐴 → ∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩})
3122, 3op2nda 5109 . . . . . . . . 9 ran {⟨𝑏, 𝑥⟩} = 𝑥
3231eqcomi 2181 . . . . . . . 8 𝑥 = ran {⟨𝑏, 𝑥⟩}
3330, 32jctir 313 . . . . . . 7 (𝑥𝐴 → (∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran {⟨𝑏, 𝑥⟩}))
34 eqeq1 2184 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑥⟩} → (𝑎 = {⟨𝑏, 𝑐⟩} ↔ {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩}))
3534rexbidv 2478 . . . . . . . 8 (𝑎 = {⟨𝑏, 𝑥⟩} → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ↔ ∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩}))
36 rneq 4850 . . . . . . . . . 10 (𝑎 = {⟨𝑏, 𝑥⟩} → ran 𝑎 = ran {⟨𝑏, 𝑥⟩})
3736unieqd 3818 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑥⟩} → ran 𝑎 = ran {⟨𝑏, 𝑥⟩})
3837eqeq2d 2189 . . . . . . . 8 (𝑎 = {⟨𝑏, 𝑥⟩} → (𝑥 = ran 𝑎𝑥 = ran {⟨𝑏, 𝑥⟩}))
3935, 38anbi12d 473 . . . . . . 7 (𝑎 = {⟨𝑏, 𝑥⟩} → ((∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎) ↔ (∃𝑐𝐴 {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran {⟨𝑏, 𝑥⟩})))
4033, 39syl5ibrcom 157 . . . . . 6 (𝑥𝐴 → (𝑎 = {⟨𝑏, 𝑥⟩} → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎)))
4140imp 124 . . . . 5 ((𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}) → (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎))
42 vex 2740 . . . . . . . . . . 11 𝑐 ∈ V
4322, 42op2nda 5109 . . . . . . . . . 10 ran {⟨𝑏, 𝑐⟩} = 𝑐
4443eqeq2i 2188 . . . . . . . . 9 (𝑥 = ran {⟨𝑏, 𝑐⟩} ↔ 𝑥 = 𝑐)
45 eqidd 2178 . . . . . . . . . . 11 (𝑐𝐴 → {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩})
4645ancli 323 . . . . . . . . . 10 (𝑐𝐴 → (𝑐𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩}))
47 eleq1w 2238 . . . . . . . . . . 11 (𝑥 = 𝑐 → (𝑥𝐴𝑐𝐴))
48 opeq2 3777 . . . . . . . . . . . . 13 (𝑥 = 𝑐 → ⟨𝑏, 𝑥⟩ = ⟨𝑏, 𝑐⟩)
4948sneqd 3604 . . . . . . . . . . . 12 (𝑥 = 𝑐 → {⟨𝑏, 𝑥⟩} = {⟨𝑏, 𝑐⟩})
5049eqeq2d 2189 . . . . . . . . . . 11 (𝑥 = 𝑐 → ({⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩} ↔ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩}))
5147, 50anbi12d 473 . . . . . . . . . 10 (𝑥 = 𝑐 → ((𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩}) ↔ (𝑐𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑐⟩})))
5246, 51syl5ibrcom 157 . . . . . . . . 9 (𝑐𝐴 → (𝑥 = 𝑐 → (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})))
5344, 52biimtrid 152 . . . . . . . 8 (𝑐𝐴 → (𝑥 = ran {⟨𝑏, 𝑐⟩} → (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})))
54 rneq 4850 . . . . . . . . . . 11 (𝑎 = {⟨𝑏, 𝑐⟩} → ran 𝑎 = ran {⟨𝑏, 𝑐⟩})
5554unieqd 3818 . . . . . . . . . 10 (𝑎 = {⟨𝑏, 𝑐⟩} → ran 𝑎 = ran {⟨𝑏, 𝑐⟩})
5655eqeq2d 2189 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑐⟩} → (𝑥 = ran 𝑎𝑥 = ran {⟨𝑏, 𝑐⟩}))
57 eqeq1 2184 . . . . . . . . . 10 (𝑎 = {⟨𝑏, 𝑐⟩} → (𝑎 = {⟨𝑏, 𝑥⟩} ↔ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩}))
5857anbi2d 464 . . . . . . . . 9 (𝑎 = {⟨𝑏, 𝑐⟩} → ((𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}) ↔ (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩})))
5956, 58imbi12d 234 . . . . . . . 8 (𝑎 = {⟨𝑏, 𝑐⟩} → ((𝑥 = ran 𝑎 → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩})) ↔ (𝑥 = ran {⟨𝑏, 𝑐⟩} → (𝑥𝐴 ∧ {⟨𝑏, 𝑐⟩} = {⟨𝑏, 𝑥⟩}))))
6053, 59syl5ibrcom 157 . . . . . . 7 (𝑐𝐴 → (𝑎 = {⟨𝑏, 𝑐⟩} → (𝑥 = ran 𝑎 → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}))))
6160rexlimiv 2588 . . . . . 6 (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} → (𝑥 = ran 𝑎 → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩})))
6261imp 124 . . . . 5 ((∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎) → (𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}))
6341, 62impbii 126 . . . 4 ((𝑥𝐴𝑎 = {⟨𝑏, 𝑥⟩}) ↔ (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎))
6425, 63bitri 184 . . 3 ((𝑥𝐴𝑎 = ({𝑏} × {𝑥})) ↔ (∃𝑐𝐴 𝑎 = {⟨𝑏, 𝑐⟩} ∧ 𝑥 = ran 𝑎))
6515, 21, 64vtoclbg 2798 . 2 (𝐼𝑉 → ((𝑥𝐴𝑎 = ({𝐼} × {𝑥})) ↔ (𝑎X𝑦 ∈ {𝐼}𝐴𝑥 = ran 𝑎)))
661, 7, 11, 65f1od 6068 1 (𝐼𝑉𝐹:𝐴1-1-ontoX𝑦 ∈ {𝐼}𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  wrex 2456  Vcvv 2737  {csn 3591  cop 3594   cuni 3807  cmpt 4061   × cxp 4621  ran crn 4624  1-1-ontowf1o 5211  Xcixp 6692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-v 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ixp 6693
This theorem is referenced by:  mapsnf1o  6731
  Copyright terms: Public domain W3C validator