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

Theorem elxp4 4996
Description: Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4997. (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 2671 . 2 (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 ∈ V)
2 elex 2671 . . . 4 ( dom {𝐴} ∈ 𝐵 dom {𝐴} ∈ V)
3 elex 2671 . . . 4 ( ran {𝐴} ∈ 𝐶 ran {𝐴} ∈ V)
42, 3anim12i 336 . . 3 (( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶) → ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V))
5 opexg 4120 . . . . 5 (( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
65adantl 275 . . . 4 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
7 eleq1 2180 . . . . 5 (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ → (𝐴 ∈ V ↔ ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V))
87adantr 274 . . . 4 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → (𝐴 ∈ V ↔ ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V))
96, 8mpbird 166 . . 3 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → 𝐴 ∈ V)
104, 9sylan2 284 . 2 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)) → 𝐴 ∈ V)
11 elxp 4526 . . . 4 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
1211a1i 9 . . 3 (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
13 sneq 3508 . . . . . . . . . . . . 13 (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
1413rneqd 4738 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
1514unieqd 3717 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
16 vex 2663 . . . . . . . . . . . 12 𝑥 ∈ V
17 vex 2663 . . . . . . . . . . . 12 𝑦 ∈ V
1816, 17op2nda 4993 . . . . . . . . . . 11 ran {⟨𝑥, 𝑦⟩} = 𝑦
1915, 18syl6req 2167 . . . . . . . . . 10 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ran {𝐴})
2019pm4.71ri 389 . . . . . . . . 9 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
2120anbi1i 453 . . . . . . . 8 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)))
22 anass 398 . . . . . . . 8 (((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2321, 22bitri 183 . . . . . . 7 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2423exbii 1569 . . . . . 6 (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
25 snexg 4078 . . . . . . . . 9 (𝐴 ∈ V → {𝐴} ∈ V)
26 rnexg 4774 . . . . . . . . 9 ({𝐴} ∈ V → ran {𝐴} ∈ V)
2725, 26syl 14 . . . . . . . 8 (𝐴 ∈ V → ran {𝐴} ∈ V)
28 uniexg 4331 . . . . . . . 8 (ran {𝐴} ∈ V → ran {𝐴} ∈ V)
2927, 28syl 14 . . . . . . 7 (𝐴 ∈ V → ran {𝐴} ∈ V)
30 opeq2 3676 . . . . . . . . . 10 (𝑦 = ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ran {𝐴}⟩)
3130eqeq2d 2129 . . . . . . . . 9 (𝑦 = ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ran {𝐴}⟩))
32 eleq1 2180 . . . . . . . . . 10 (𝑦 = ran {𝐴} → (𝑦𝐶 ran {𝐴} ∈ 𝐶))
3332anbi2d 459 . . . . . . . . 9 (𝑦 = ran {𝐴} → ((𝑥𝐵𝑦𝐶) ↔ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))
3431, 33anbi12d 464 . . . . . . . 8 (𝑦 = ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3534ceqsexgv 2788 . . . . . . 7 ( ran {𝐴} ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3629, 35syl 14 . . . . . 6 (𝐴 ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3724, 36syl5bb 191 . . . . 5 (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
38 sneq 3508 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → {𝐴} = {⟨𝑥, ran {𝐴}⟩})
3938dmeqd 4711 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4039unieqd 3717 . . . . . . . . . 10 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4140adantl 275 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
42 dmsnopg 4980 . . . . . . . . . . . . 13 ( ran {𝐴} ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4329, 42syl 14 . . . . . . . . . . . 12 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4443unieqd 3717 . . . . . . . . . . 11 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4516unisn 3722 . . . . . . . . . . 11 {𝑥} = 𝑥
4644, 45syl6eq 2166 . . . . . . . . . 10 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4746adantr 274 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4841, 47eqtr2d 2151 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → 𝑥 = dom {𝐴})
4948ex 114 . . . . . . 7 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ → 𝑥 = dom {𝐴}))
5049pm4.71rd 391 . . . . . 6 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ (𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩)))
5150anbi1d 460 . . . . 5 (𝐴 ∈ V → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
52 anass 398 . . . . . 6 (((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
5352a1i 9 . . . . 5 (𝐴 ∈ V → (((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
5437, 51, 533bitrd 213 . . . 4 (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
5554exbidv 1781 . . 3 (𝐴 ∈ V → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑥(𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
56 dmexg 4773 . . . . . 6 ({𝐴} ∈ V → dom {𝐴} ∈ V)
5725, 56syl 14 . . . . 5 (𝐴 ∈ V → dom {𝐴} ∈ V)
58 uniexg 4331 . . . . 5 (dom {𝐴} ∈ V → dom {𝐴} ∈ V)
5957, 58syl 14 . . . 4 (𝐴 ∈ V → dom {𝐴} ∈ V)
60 opeq1 3675 . . . . . . 7 (𝑥 = dom {𝐴} → ⟨𝑥, ran {𝐴}⟩ = ⟨ dom {𝐴}, ran {𝐴}⟩)
6160eqeq2d 2129 . . . . . 6 (𝑥 = dom {𝐴} → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ 𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩))
62 eleq1 2180 . . . . . . 7 (𝑥 = dom {𝐴} → (𝑥𝐵 dom {𝐴} ∈ 𝐵))
6362anbi1d 460 . . . . . 6 (𝑥 = dom {𝐴} → ((𝑥𝐵 ran {𝐴} ∈ 𝐶) ↔ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
6461, 63anbi12d 464 . . . . 5 (𝑥 = dom {𝐴} → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
6564ceqsexgv 2788 . . . 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 213 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
681, 10, 67pm5.21nii 678 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104   = wceq 1316  wex 1453  wcel 1465  Vcvv 2660  {csn 3497  cop 3500   cuni 3706   × cxp 4507  dom cdm 4509  ran crn 4510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-pow 4068  ax-pr 4101  ax-un 4325
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-un 3045  df-in 3047  df-ss 3054  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-opab 3960  df-xp 4515  df-rel 4516  df-cnv 4517  df-dm 4519  df-rn 4520
This theorem is referenced by:  elxp6  6035  xpdom2  6693
  Copyright terms: Public domain W3C validator