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

Theorem dfco2a 4808
Description: Generalization of dfco2 4807, where 𝐶 can have any value between dom 𝐴 ∩ ran 𝐵 and V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
dfco2a ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴𝐵) = 𝑥𝐶 ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶

Proof of Theorem dfco2a
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfco2 4807 . 2 (𝐴𝐵) = 𝑥 ∈ V ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))
2 vex 2557 . . . . . . . . . . . . . 14 𝑥 ∈ V
3 vex 2557 . . . . . . . . . . . . . . 15 𝑧 ∈ V
43eliniseg 4682 . . . . . . . . . . . . . 14 (𝑥 ∈ V → (𝑧 ∈ (𝐵 “ {𝑥}) ↔ 𝑧𝐵𝑥))
52, 4ax-mp 7 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐵 “ {𝑥}) ↔ 𝑧𝐵𝑥)
63, 2brelrn 4554 . . . . . . . . . . . . 13 (𝑧𝐵𝑥𝑥 ∈ ran 𝐵)
75, 6sylbi 114 . . . . . . . . . . . 12 (𝑧 ∈ (𝐵 “ {𝑥}) → 𝑥 ∈ ran 𝐵)
8 vex 2557 . . . . . . . . . . . . . 14 𝑤 ∈ V
92, 8elimasn 4679 . . . . . . . . . . . . 13 (𝑤 ∈ (𝐴 “ {𝑥}) ↔ ⟨𝑥, 𝑤⟩ ∈ 𝐴)
102, 8opeldm 4525 . . . . . . . . . . . . 13 (⟨𝑥, 𝑤⟩ ∈ 𝐴𝑥 ∈ dom 𝐴)
119, 10sylbi 114 . . . . . . . . . . . 12 (𝑤 ∈ (𝐴 “ {𝑥}) → 𝑥 ∈ dom 𝐴)
127, 11anim12ci 322 . . . . . . . . . . 11 ((𝑧 ∈ (𝐵 “ {𝑥}) ∧ 𝑤 ∈ (𝐴 “ {𝑥})) → (𝑥 ∈ dom 𝐴𝑥 ∈ ran 𝐵))
1312adantl 262 . . . . . . . . . 10 ((𝑦 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ (𝐵 “ {𝑥}) ∧ 𝑤 ∈ (𝐴 “ {𝑥}))) → (𝑥 ∈ dom 𝐴𝑥 ∈ ran 𝐵))
1413exlimivv 1776 . . . . . . . . 9 (∃𝑧𝑤(𝑦 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ (𝐵 “ {𝑥}) ∧ 𝑤 ∈ (𝐴 “ {𝑥}))) → (𝑥 ∈ dom 𝐴𝑥 ∈ ran 𝐵))
15 elxp 4349 . . . . . . . . 9 (𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑧𝑤(𝑦 = ⟨𝑧, 𝑤⟩ ∧ (𝑧 ∈ (𝐵 “ {𝑥}) ∧ 𝑤 ∈ (𝐴 “ {𝑥}))))
16 elin 3123 . . . . . . . . 9 (𝑥 ∈ (dom 𝐴 ∩ ran 𝐵) ↔ (𝑥 ∈ dom 𝐴𝑥 ∈ ran 𝐵))
1714, 15, 163imtr4i 190 . . . . . . . 8 (𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) → 𝑥 ∈ (dom 𝐴 ∩ ran 𝐵))
18 ssel 2936 . . . . . . . 8 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝑥 ∈ (dom 𝐴 ∩ ran 𝐵) → 𝑥𝐶))
1917, 18syl5 28 . . . . . . 7 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) → 𝑥𝐶))
2019pm4.71rd 374 . . . . . 6 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ (𝑥𝐶𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))))
2120exbidv 1706 . . . . 5 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (∃𝑥 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥(𝑥𝐶𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))))
22 rexv 2569 . . . . 5 (∃𝑥 ∈ V 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
23 df-rex 2309 . . . . 5 (∃𝑥𝐶 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥(𝑥𝐶𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))))
2421, 22, 233bitr4g 212 . . . 4 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (∃𝑥 ∈ V 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥𝐶 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))))
25 eliun 3658 . . . 4 (𝑦 𝑥 ∈ V ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥 ∈ V 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
26 eliun 3658 . . . 4 (𝑦 𝑥𝐶 ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ ∃𝑥𝐶 𝑦 ∈ ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
2724, 25, 263bitr4g 212 . . 3 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝑦 𝑥 ∈ V ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) ↔ 𝑦 𝑥𝐶 ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))))
2827eqrdv 2038 . 2 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 𝑥 ∈ V ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) = 𝑥𝐶 ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
291, 28syl5eq 2084 1 ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴𝐵) = 𝑥𝐶 ((𝐵 “ {𝑥}) × (𝐴 “ {𝑥})))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wb 98   = wceq 1243  wex 1381  wcel 1393  wrex 2304  Vcvv 2554  cin 2913  wss 2914  {csn 3372  cop 3375   ciun 3654   class class class wbr 3761   × cxp 4330  ccnv 4331  dom cdm 4332  ran crn 4333  cima 4335  ccom 4336
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3872  ax-pow 3924  ax-pr 3941
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-rex 2309  df-v 2556  df-sbc 2762  df-un 2919  df-in 2921  df-ss 2928  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-iun 3656  df-br 3762  df-opab 3816  df-xp 4338  df-rel 4339  df-cnv 4340  df-co 4341  df-dm 4342  df-rn 4343  df-res 4344  df-ima 4345
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator