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

Theorem elxp4 4875
Description: Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4876. (Contributed by NM, 17-Feb-2004.)
Assertion
Ref Expression
elxp4 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))

Proof of Theorem elxp4
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2623 . 2 (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 ∈ V)
2 elex 2623 . . . 4 ( dom {𝐴} ∈ 𝐵 dom {𝐴} ∈ V)
3 elex 2623 . . . 4 ( ran {𝐴} ∈ 𝐶 ran {𝐴} ∈ V)
42, 3anim12i 331 . . 3 (( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶) → ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V))
5 opexg 4022 . . . . 5 (( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
65adantl 271 . . . 4 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
7 eleq1 2147 . . . . 5 (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ → (𝐴 ∈ V ↔ ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V))
87adantr 270 . . . 4 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → (𝐴 ∈ V ↔ ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V))
96, 8mpbird 165 . . 3 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → 𝐴 ∈ V)
104, 9sylan2 280 . 2 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)) → 𝐴 ∈ V)
11 elxp 4421 . . . 4 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
1211a1i 9 . . 3 (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
13 sneq 3436 . . . . . . . . . . . . 13 (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
1413rneqd 4625 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
1514unieqd 3641 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
16 vex 2617 . . . . . . . . . . . 12 𝑥 ∈ V
17 vex 2617 . . . . . . . . . . . 12 𝑦 ∈ V
1816, 17op2nda 4872 . . . . . . . . . . 11 ran {⟨𝑥, 𝑦⟩} = 𝑦
1915, 18syl6req 2134 . . . . . . . . . 10 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ran {𝐴})
2019pm4.71ri 384 . . . . . . . . 9 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
2120anbi1i 446 . . . . . . . 8 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)))
22 anass 393 . . . . . . . 8 (((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2321, 22bitri 182 . . . . . . 7 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2423exbii 1539 . . . . . 6 (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
25 snexg 3986 . . . . . . . . 9 (𝐴 ∈ V → {𝐴} ∈ V)
26 rnexg 4659 . . . . . . . . 9 ({𝐴} ∈ V → ran {𝐴} ∈ V)
2725, 26syl 14 . . . . . . . 8 (𝐴 ∈ V → ran {𝐴} ∈ V)
28 uniexg 4232 . . . . . . . 8 (ran {𝐴} ∈ V → ran {𝐴} ∈ V)
2927, 28syl 14 . . . . . . 7 (𝐴 ∈ V → ran {𝐴} ∈ V)
30 opeq2 3600 . . . . . . . . . 10 (𝑦 = ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ran {𝐴}⟩)
3130eqeq2d 2096 . . . . . . . . 9 (𝑦 = ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ran {𝐴}⟩))
32 eleq1 2147 . . . . . . . . . 10 (𝑦 = ran {𝐴} → (𝑦𝐶 ran {𝐴} ∈ 𝐶))
3332anbi2d 452 . . . . . . . . 9 (𝑦 = ran {𝐴} → ((𝑥𝐵𝑦𝐶) ↔ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))
3431, 33anbi12d 457 . . . . . . . 8 (𝑦 = ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3534ceqsexgv 2736 . . . . . . 7 ( ran {𝐴} ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3629, 35syl 14 . . . . . 6 (𝐴 ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3724, 36syl5bb 190 . . . . 5 (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
38 sneq 3436 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → {𝐴} = {⟨𝑥, ran {𝐴}⟩})
3938dmeqd 4599 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4039unieqd 3641 . . . . . . . . . 10 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4140adantl 271 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
42 dmsnopg 4859 . . . . . . . . . . . . 13 ( ran {𝐴} ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4329, 42syl 14 . . . . . . . . . . . 12 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4443unieqd 3641 . . . . . . . . . . 11 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4516unisn 3646 . . . . . . . . . . 11 {𝑥} = 𝑥
4644, 45syl6eq 2133 . . . . . . . . . 10 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4746adantr 270 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4841, 47eqtr2d 2118 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → 𝑥 = dom {𝐴})
4948ex 113 . . . . . . 7 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ → 𝑥 = dom {𝐴}))
5049pm4.71rd 386 . . . . . 6 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ (𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩)))
5150anbi1d 453 . . . . 5 (𝐴 ∈ V → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
52 anass 393 . . . . . 6 (((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
5352a1i 9 . . . . 5 (𝐴 ∈ V → (((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
5437, 51, 533bitrd 212 . . . 4 (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
5554exbidv 1750 . . 3 (𝐴 ∈ V → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑥(𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
56 dmexg 4658 . . . . . 6 ({𝐴} ∈ V → dom {𝐴} ∈ V)
5725, 56syl 14 . . . . 5 (𝐴 ∈ V → dom {𝐴} ∈ V)
58 uniexg 4232 . . . . 5 (dom {𝐴} ∈ V → dom {𝐴} ∈ V)
5957, 58syl 14 . . . 4 (𝐴 ∈ V → dom {𝐴} ∈ V)
60 opeq1 3599 . . . . . . 7 (𝑥 = dom {𝐴} → ⟨𝑥, ran {𝐴}⟩ = ⟨ dom {𝐴}, ran {𝐴}⟩)
6160eqeq2d 2096 . . . . . 6 (𝑥 = dom {𝐴} → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ 𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩))
62 eleq1 2147 . . . . . . 7 (𝑥 = dom {𝐴} → (𝑥𝐵 dom {𝐴} ∈ 𝐵))
6362anbi1d 453 . . . . . 6 (𝑥 = dom {𝐴} → ((𝑥𝐵 ran {𝐴} ∈ 𝐶) ↔ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
6461, 63anbi12d 457 . . . . 5 (𝑥 = dom {𝐴} → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
6564ceqsexgv 2736 . . . 4 ( dom {𝐴} ∈ V → (∃𝑥(𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
6659, 65syl 14 . . 3 (𝐴 ∈ V → (∃𝑥(𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
6712, 55, 663bitrd 212 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
681, 10, 67pm5.21nii 653 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103   = wceq 1287  wex 1424  wcel 1436  Vcvv 2614  {csn 3425  cop 3428   cuni 3630   × cxp 4402  dom cdm 4404  ran crn 4405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925  ax-pow 3977  ax-pr 4003  ax-un 4227
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2616  df-un 2990  df-in 2992  df-ss 2999  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-br 3815  df-opab 3869  df-xp 4410  df-rel 4411  df-cnv 4412  df-dm 4414  df-rn 4415
This theorem is referenced by:  elxp6  5878  xpdom2  6480
  Copyright terms: Public domain W3C validator