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

Theorem elxp4 5033
Description: Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 5034. (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 2700 . 2 (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 ∈ V)
2 elex 2700 . . . 4 ( dom {𝐴} ∈ 𝐵 dom {𝐴} ∈ V)
3 elex 2700 . . . 4 ( ran {𝐴} ∈ 𝐶 ran {𝐴} ∈ V)
42, 3anim12i 336 . . 3 (( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶) → ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V))
5 opexg 4157 . . . . 5 (( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
65adantl 275 . . . 4 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
7 eleq1 2203 . . . . 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 4563 . . . 4 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
1211a1i 9 . . 3 (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
13 sneq 3542 . . . . . . . . . . . . 13 (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
1413rneqd 4775 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
1514unieqd 3754 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
16 vex 2692 . . . . . . . . . . . 12 𝑥 ∈ V
17 vex 2692 . . . . . . . . . . . 12 𝑦 ∈ V
1816, 17op2nda 5030 . . . . . . . . . . 11 ran {⟨𝑥, 𝑦⟩} = 𝑦
1915, 18eqtr2di 2190 . . . . . . . . . 10 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ran {𝐴})
2019pm4.71ri 390 . . . . . . . . 9 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
2120anbi1i 454 . . . . . . . 8 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)))
22 anass 399 . . . . . . . 8 (((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2321, 22bitri 183 . . . . . . 7 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2423exbii 1585 . . . . . 6 (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
25 snexg 4115 . . . . . . . . 9 (𝐴 ∈ V → {𝐴} ∈ V)
26 rnexg 4811 . . . . . . . . 9 ({𝐴} ∈ V → ran {𝐴} ∈ V)
2725, 26syl 14 . . . . . . . 8 (𝐴 ∈ V → ran {𝐴} ∈ V)
28 uniexg 4368 . . . . . . . 8 (ran {𝐴} ∈ V → ran {𝐴} ∈ V)
2927, 28syl 14 . . . . . . 7 (𝐴 ∈ V → ran {𝐴} ∈ V)
30 opeq2 3713 . . . . . . . . . 10 (𝑦 = ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ran {𝐴}⟩)
3130eqeq2d 2152 . . . . . . . . 9 (𝑦 = ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ran {𝐴}⟩))
32 eleq1 2203 . . . . . . . . . 10 (𝑦 = ran {𝐴} → (𝑦𝐶 ran {𝐴} ∈ 𝐶))
3332anbi2d 460 . . . . . . . . 9 (𝑦 = ran {𝐴} → ((𝑥𝐵𝑦𝐶) ↔ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))
3431, 33anbi12d 465 . . . . . . . 8 (𝑦 = ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3534ceqsexgv 2817 . . . . . . 7 ( ran {𝐴} ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3629, 35syl 14 . . . . . 6 (𝐴 ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3724, 36syl5bb 191 . . . . 5 (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
38 sneq 3542 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → {𝐴} = {⟨𝑥, ran {𝐴}⟩})
3938dmeqd 4748 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4039unieqd 3754 . . . . . . . . . 10 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4140adantl 275 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
42 dmsnopg 5017 . . . . . . . . . . . . 13 ( ran {𝐴} ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4329, 42syl 14 . . . . . . . . . . . 12 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4443unieqd 3754 . . . . . . . . . . 11 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4516unisn 3759 . . . . . . . . . . 11 {𝑥} = 𝑥
4644, 45eqtrdi 2189 . . . . . . . . . 10 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4746adantr 274 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4841, 47eqtr2d 2174 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → 𝑥 = dom {𝐴})
4948ex 114 . . . . . . 7 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ → 𝑥 = dom {𝐴}))
5049pm4.71rd 392 . . . . . 6 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ (𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩)))
5150anbi1d 461 . . . . 5 (𝐴 ∈ V → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
52 anass 399 . . . . . 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 1798 . . 3 (𝐴 ∈ V → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑥(𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
56 dmexg 4810 . . . . . 6 ({𝐴} ∈ V → dom {𝐴} ∈ V)
5725, 56syl 14 . . . . 5 (𝐴 ∈ V → dom {𝐴} ∈ V)
58 uniexg 4368 . . . . 5 (dom {𝐴} ∈ V → dom {𝐴} ∈ V)
5957, 58syl 14 . . . 4 (𝐴 ∈ V → dom {𝐴} ∈ V)
60 opeq1 3712 . . . . . . 7 (𝑥 = dom {𝐴} → ⟨𝑥, ran {𝐴}⟩ = ⟨ dom {𝐴}, ran {𝐴}⟩)
6160eqeq2d 2152 . . . . . 6 (𝑥 = dom {𝐴} → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ 𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩))
62 eleq1 2203 . . . . . . 7 (𝑥 = dom {𝐴} → (𝑥𝐵 dom {𝐴} ∈ 𝐵))
6362anbi1d 461 . . . . . 6 (𝑥 = dom {𝐴} → ((𝑥𝐵 ran {𝐴} ∈ 𝐶) ↔ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
6461, 63anbi12d 465 . . . . 5 (𝑥 = dom {𝐴} → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
6564ceqsexgv 2817 . . . 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 694 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104   = wceq 1332  wex 1469  wcel 1481  Vcvv 2689  {csn 3531  cop 3534   cuni 3743   × cxp 4544  dom cdm 4546  ran crn 4547
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-opab 3997  df-xp 4552  df-rel 4553  df-cnv 4554  df-dm 4556  df-rn 4557
This theorem is referenced by:  elxp6  6074  xpdom2  6732
  Copyright terms: Public domain W3C validator