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

Theorem elxp4 4808
Description: Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4809. (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 2566 . 2 (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 ∈ V)
2 elex 2566 . . . 4 ( dom {𝐴} ∈ 𝐵 dom {𝐴} ∈ V)
3 elex 2566 . . . 4 ( ran {𝐴} ∈ 𝐶 ran {𝐴} ∈ V)
42, 3anim12i 321 . . 3 (( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶) → ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V))
5 opexgOLD 3965 . . . . 5 (( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
65adantl 262 . . . 4 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V)
7 eleq1 2100 . . . . 5 (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ → (𝐴 ∈ V ↔ ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V))
87adantr 261 . . . 4 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → (𝐴 ∈ V ↔ ⟨ dom {𝐴}, ran {𝐴}⟩ ∈ V))
96, 8mpbird 156 . . 3 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ V ∧ ran {𝐴} ∈ V)) → 𝐴 ∈ V)
104, 9sylan2 270 . 2 ((𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)) → 𝐴 ∈ V)
11 elxp 4362 . . . 4 (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)))
1211a1i 9 . . 3 (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
13 sneq 3386 . . . . . . . . . . . . 13 (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩})
1413rneqd 4563 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
1514unieqd 3591 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩})
16 vex 2560 . . . . . . . . . . . 12 𝑥 ∈ V
17 vex 2560 . . . . . . . . . . . 12 𝑦 ∈ V
1816, 17op2nda 4805 . . . . . . . . . . 11 ran {⟨𝑥, 𝑦⟩} = 𝑦
1915, 18syl6req 2089 . . . . . . . . . 10 (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ran {𝐴})
2019pm4.71ri 372 . . . . . . . . 9 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩))
2120anbi1i 431 . . . . . . . 8 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)))
22 anass 381 . . . . . . . 8 (((𝑦 = ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2321, 22bitri 173 . . . . . . 7 ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
2423exbii 1496 . . . . . 6 (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))))
25 snexgOLD 3935 . . . . . . . . 9 (𝐴 ∈ V → {𝐴} ∈ V)
26 rnexg 4597 . . . . . . . . 9 ({𝐴} ∈ V → ran {𝐴} ∈ V)
2725, 26syl 14 . . . . . . . 8 (𝐴 ∈ V → ran {𝐴} ∈ V)
28 uniexg 4175 . . . . . . . 8 (ran {𝐴} ∈ V → ran {𝐴} ∈ V)
2927, 28syl 14 . . . . . . 7 (𝐴 ∈ V → ran {𝐴} ∈ V)
30 opeq2 3550 . . . . . . . . . 10 (𝑦 = ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ran {𝐴}⟩)
3130eqeq2d 2051 . . . . . . . . 9 (𝑦 = ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ran {𝐴}⟩))
32 eleq1 2100 . . . . . . . . . 10 (𝑦 = ran {𝐴} → (𝑦𝐶 ran {𝐴} ∈ 𝐶))
3332anbi2d 437 . . . . . . . . 9 (𝑦 = ran {𝐴} → ((𝑥𝐵𝑦𝐶) ↔ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))
3431, 33anbi12d 442 . . . . . . . 8 (𝑦 = ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3534ceqsexgv 2673 . . . . . . 7 ( ran {𝐴} ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3629, 35syl 14 . . . . . 6 (𝐴 ∈ V → (∃𝑦(𝑦 = ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶))) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
3724, 36syl5bb 181 . . . . 5 (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
38 sneq 3386 . . . . . . . . . . . 12 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → {𝐴} = {⟨𝑥, ran {𝐴}⟩})
3938dmeqd 4537 . . . . . . . . . . 11 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4039unieqd 3591 . . . . . . . . . 10 (𝐴 = ⟨𝑥, ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
4140adantl 262 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {𝐴} = dom {⟨𝑥, ran {𝐴}⟩})
42 dmsnopg 4792 . . . . . . . . . . . . 13 ( ran {𝐴} ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4329, 42syl 14 . . . . . . . . . . . 12 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4443unieqd 3591 . . . . . . . . . . 11 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = {𝑥})
4516unisn 3596 . . . . . . . . . . 11 {𝑥} = 𝑥
4644, 45syl6eq 2088 . . . . . . . . . 10 (𝐴 ∈ V → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4746adantr 261 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → dom {⟨𝑥, ran {𝐴}⟩} = 𝑥)
4841, 47eqtr2d 2073 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) → 𝑥 = dom {𝐴})
4948ex 108 . . . . . . 7 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ → 𝑥 = dom {𝐴}))
5049pm4.71rd 374 . . . . . 6 (𝐴 ∈ V → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ (𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩)))
5150anbi1d 438 . . . . 5 (𝐴 ∈ V → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ ((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
52 anass 381 . . . . . 6 (((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶))))
5352a1i 9 . . . . 5 (𝐴 ∈ V → (((𝑥 = dom {𝐴} ∧ 𝐴 = ⟨𝑥, ran {𝐴}⟩) ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
5437, 51, 533bitrd 203 . . . 4 (𝐴 ∈ V → (∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ (𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
5554exbidv 1706 . . 3 (𝐴 ∈ V → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐵𝑦𝐶)) ↔ ∃𝑥(𝑥 = dom {𝐴} ∧ (𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)))))
56 dmexg 4596 . . . . . 6 ({𝐴} ∈ V → dom {𝐴} ∈ V)
5725, 56syl 14 . . . . 5 (𝐴 ∈ V → dom {𝐴} ∈ V)
58 uniexg 4175 . . . . 5 (dom {𝐴} ∈ V → dom {𝐴} ∈ V)
5957, 58syl 14 . . . 4 (𝐴 ∈ V → dom {𝐴} ∈ V)
60 opeq1 3549 . . . . . . 7 (𝑥 = dom {𝐴} → ⟨𝑥, ran {𝐴}⟩ = ⟨ dom {𝐴}, ran {𝐴}⟩)
6160eqeq2d 2051 . . . . . 6 (𝑥 = dom {𝐴} → (𝐴 = ⟨𝑥, ran {𝐴}⟩ ↔ 𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩))
62 eleq1 2100 . . . . . . 7 (𝑥 = dom {𝐴} → (𝑥𝐵 dom {𝐴} ∈ 𝐵))
6362anbi1d 438 . . . . . 6 (𝑥 = dom {𝐴} → ((𝑥𝐵 ran {𝐴} ∈ 𝐶) ↔ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
6461, 63anbi12d 442 . . . . 5 (𝑥 = dom {𝐴} → ((𝐴 = ⟨𝑥, ran {𝐴}⟩ ∧ (𝑥𝐵 ran {𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
6564ceqsexgv 2673 . . . 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 203 . 2 (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶))))
681, 10, 67pm5.21nii 620 1 (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨ dom {𝐴}, ran {𝐴}⟩ ∧ ( dom {𝐴} ∈ 𝐵 ran {𝐴} ∈ 𝐶)))
Colors of variables: wff set class
Syntax hints:  wa 97  wb 98   = wceq 1243  wex 1381  wcel 1393  Vcvv 2557  {csn 3375  cop 3378   cuni 3580   × cxp 4343  dom cdm 4345  ran crn 4346
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-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944  ax-un 4170
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 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-xp 4351  df-rel 4352  df-cnv 4353  df-dm 4355  df-rn 4356
This theorem is referenced by:  elxp6  5796  xpdom2  6305
  Copyright terms: Public domain W3C validator