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

Theorem xpdom2 6241
Description: Dominance law for Cartesian product. Proposition 10.33(2) of [TakeutiZaring] p. 92. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
Hypothesis
Ref Expression
xpdom.2 𝐶 V
Assertion
Ref Expression
xpdom2 (AB → (𝐶 × A) ≼ (𝐶 × B))

Proof of Theorem xpdom2
Dummy variables u f v w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdomi 6166 . 2 (ABf f:A1-1B)
2 f1f 5035 . . . . . . . 8 (f:A1-1Bf:AB)
3 ffvelrn 5243 . . . . . . . . 9 ((f:AB ran {x} A) → (f ran {x}) B)
43ex 108 . . . . . . . 8 (f:AB → ( ran {x} A → (f ran {x}) B))
52, 4syl 14 . . . . . . 7 (f:A1-1B → ( ran {x} A → (f ran {x}) B))
65anim2d 320 . . . . . 6 (f:A1-1B → (( dom {x} 𝐶 ran {x} A) → ( dom {x} 𝐶 (f ran {x}) B)))
76adantld 263 . . . . 5 (f:A1-1B → ((x = ⟨ dom {x}, ran {x}⟩ ( dom {x} 𝐶 ran {x} A)) → ( dom {x} 𝐶 (f ran {x}) B)))
8 elxp4 4751 . . . . 5 (x (𝐶 × A) ↔ (x = ⟨ dom {x}, ran {x}⟩ ( dom {x} 𝐶 ran {x} A)))
9 opelxp 4317 . . . . 5 (⟨ dom {x}, (f ran {x})⟩ (𝐶 × B) ↔ ( dom {x} 𝐶 (f ran {x}) B))
107, 8, 93imtr4g 194 . . . 4 (f:A1-1B → (x (𝐶 × A) → ⟨ dom {x}, (f ran {x})⟩ (𝐶 × B)))
1110adantl 262 . . 3 ((AB f:A1-1B) → (x (𝐶 × A) → ⟨ dom {x}, (f ran {x})⟩ (𝐶 × B)))
12 elxp2 4306 . . . . . 6 (x (𝐶 × A) ↔ z 𝐶 w A x = ⟨z, w⟩)
13 elxp2 4306 . . . . . 6 (y (𝐶 × A) ↔ v 𝐶 u A y = ⟨v, u⟩)
14 vex 2554 . . . . . . . . . . . . . . . . . 18 z V
15 vex 2554 . . . . . . . . . . . . . . . . . . 19 f V
16 vex 2554 . . . . . . . . . . . . . . . . . . 19 w V
1715, 16fvex 5138 . . . . . . . . . . . . . . . . . 18 (fw) V
1814, 17opth 3965 . . . . . . . . . . . . . . . . 17 (⟨z, (fw)⟩ = ⟨v, (fu)⟩ ↔ (z = v (fw) = (fu)))
19 f1fveq 5354 . . . . . . . . . . . . . . . . . . 19 ((f:A1-1B (w A u A)) → ((fw) = (fu) ↔ w = u))
2019ancoms 255 . . . . . . . . . . . . . . . . . 18 (((w A u A) f:A1-1B) → ((fw) = (fu) ↔ w = u))
2120anbi2d 437 . . . . . . . . . . . . . . . . 17 (((w A u A) f:A1-1B) → ((z = v (fw) = (fu)) ↔ (z = v w = u)))
2218, 21syl5bb 181 . . . . . . . . . . . . . . . 16 (((w A u A) f:A1-1B) → (⟨z, (fw)⟩ = ⟨v, (fu)⟩ ↔ (z = v w = u)))
2322ex 108 . . . . . . . . . . . . . . 15 ((w A u A) → (f:A1-1B → (⟨z, (fw)⟩ = ⟨v, (fu)⟩ ↔ (z = v w = u))))
2423ad2ant2l 477 . . . . . . . . . . . . . 14 (((z 𝐶 w A) (v 𝐶 u A)) → (f:A1-1B → (⟨z, (fw)⟩ = ⟨v, (fu)⟩ ↔ (z = v w = u))))
2524imp 115 . . . . . . . . . . . . 13 ((((z 𝐶 w A) (v 𝐶 u A)) f:A1-1B) → (⟨z, (fw)⟩ = ⟨v, (fu)⟩ ↔ (z = v w = u)))
2625adantlr 446 . . . . . . . . . . . 12 (((((z 𝐶 w A) (v 𝐶 u A)) (x = ⟨z, w y = ⟨v, u⟩)) f:A1-1B) → (⟨z, (fw)⟩ = ⟨v, (fu)⟩ ↔ (z = v w = u)))
27 sneq 3378 . . . . . . . . . . . . . . . . . 18 (x = ⟨z, w⟩ → {x} = {⟨z, w⟩})
2827dmeqd 4480 . . . . . . . . . . . . . . . . 17 (x = ⟨z, w⟩ → dom {x} = dom {⟨z, w⟩})
2928unieqd 3582 . . . . . . . . . . . . . . . 16 (x = ⟨z, w⟩ → dom {x} = dom {⟨z, w⟩})
3014, 16op1sta 4745 . . . . . . . . . . . . . . . 16 dom {⟨z, w⟩} = z
3129, 30syl6eq 2085 . . . . . . . . . . . . . . 15 (x = ⟨z, w⟩ → dom {x} = z)
3227rneqd 4506 . . . . . . . . . . . . . . . . . 18 (x = ⟨z, w⟩ → ran {x} = ran {⟨z, w⟩})
3332unieqd 3582 . . . . . . . . . . . . . . . . 17 (x = ⟨z, w⟩ → ran {x} = ran {⟨z, w⟩})
3414, 16op2nda 4748 . . . . . . . . . . . . . . . . 17 ran {⟨z, w⟩} = w
3533, 34syl6eq 2085 . . . . . . . . . . . . . . . 16 (x = ⟨z, w⟩ → ran {x} = w)
3635fveq2d 5125 . . . . . . . . . . . . . . 15 (x = ⟨z, w⟩ → (f ran {x}) = (fw))
3731, 36opeq12d 3548 . . . . . . . . . . . . . 14 (x = ⟨z, w⟩ → ⟨ dom {x}, (f ran {x})⟩ = ⟨z, (fw)⟩)
38 sneq 3378 . . . . . . . . . . . . . . . . . 18 (y = ⟨v, u⟩ → {y} = {⟨v, u⟩})
3938dmeqd 4480 . . . . . . . . . . . . . . . . 17 (y = ⟨v, u⟩ → dom {y} = dom {⟨v, u⟩})
4039unieqd 3582 . . . . . . . . . . . . . . . 16 (y = ⟨v, u⟩ → dom {y} = dom {⟨v, u⟩})
41 vex 2554 . . . . . . . . . . . . . . . . 17 v V
42 vex 2554 . . . . . . . . . . . . . . . . 17 u V
4341, 42op1sta 4745 . . . . . . . . . . . . . . . 16 dom {⟨v, u⟩} = v
4440, 43syl6eq 2085 . . . . . . . . . . . . . . 15 (y = ⟨v, u⟩ → dom {y} = v)
4538rneqd 4506 . . . . . . . . . . . . . . . . . 18 (y = ⟨v, u⟩ → ran {y} = ran {⟨v, u⟩})
4645unieqd 3582 . . . . . . . . . . . . . . . . 17 (y = ⟨v, u⟩ → ran {y} = ran {⟨v, u⟩})
4741, 42op2nda 4748 . . . . . . . . . . . . . . . . 17 ran {⟨v, u⟩} = u
4846, 47syl6eq 2085 . . . . . . . . . . . . . . . 16 (y = ⟨v, u⟩ → ran {y} = u)
4948fveq2d 5125 . . . . . . . . . . . . . . 15 (y = ⟨v, u⟩ → (f ran {y}) = (fu))
5044, 49opeq12d 3548 . . . . . . . . . . . . . 14 (y = ⟨v, u⟩ → ⟨ dom {y}, (f ran {y})⟩ = ⟨v, (fu)⟩)
5137, 50eqeqan12d 2052 . . . . . . . . . . . . 13 ((x = ⟨z, w y = ⟨v, u⟩) → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ ⟨z, (fw)⟩ = ⟨v, (fu)⟩))
5251ad2antlr 458 . . . . . . . . . . . 12 (((((z 𝐶 w A) (v 𝐶 u A)) (x = ⟨z, w y = ⟨v, u⟩)) f:A1-1B) → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ ⟨z, (fw)⟩ = ⟨v, (fu)⟩))
53 eqeq12 2049 . . . . . . . . . . . . . 14 ((x = ⟨z, w y = ⟨v, u⟩) → (x = y ↔ ⟨z, w⟩ = ⟨v, u⟩))
5414, 16opth 3965 . . . . . . . . . . . . . 14 (⟨z, w⟩ = ⟨v, u⟩ ↔ (z = v w = u))
5553, 54syl6bb 185 . . . . . . . . . . . . 13 ((x = ⟨z, w y = ⟨v, u⟩) → (x = y ↔ (z = v w = u)))
5655ad2antlr 458 . . . . . . . . . . . 12 (((((z 𝐶 w A) (v 𝐶 u A)) (x = ⟨z, w y = ⟨v, u⟩)) f:A1-1B) → (x = y ↔ (z = v w = u)))
5726, 52, 563bitr4d 209 . . . . . . . . . . 11 (((((z 𝐶 w A) (v 𝐶 u A)) (x = ⟨z, w y = ⟨v, u⟩)) f:A1-1B) → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y))
5857exp53 359 . . . . . . . . . 10 ((z 𝐶 w A) → ((v 𝐶 u A) → (x = ⟨z, w⟩ → (y = ⟨v, u⟩ → (f:A1-1B → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y))))))
5958com23 72 . . . . . . . . 9 ((z 𝐶 w A) → (x = ⟨z, w⟩ → ((v 𝐶 u A) → (y = ⟨v, u⟩ → (f:A1-1B → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y))))))
6059rexlimivv 2432 . . . . . . . 8 (z 𝐶 w A x = ⟨z, w⟩ → ((v 𝐶 u A) → (y = ⟨v, u⟩ → (f:A1-1B → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y)))))
6160rexlimdvv 2433 . . . . . . 7 (z 𝐶 w A x = ⟨z, w⟩ → (v 𝐶 u A y = ⟨v, u⟩ → (f:A1-1B → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y))))
6261imp 115 . . . . . 6 ((z 𝐶 w A x = ⟨z, w v 𝐶 u A y = ⟨v, u⟩) → (f:A1-1B → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y)))
6312, 13, 62syl2anb 275 . . . . 5 ((x (𝐶 × A) y (𝐶 × A)) → (f:A1-1B → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y)))
6463com12 27 . . . 4 (f:A1-1B → ((x (𝐶 × A) y (𝐶 × A)) → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y)))
6564adantl 262 . . 3 ((AB f:A1-1B) → ((x (𝐶 × A) y (𝐶 × A)) → (⟨ dom {x}, (f ran {x})⟩ = ⟨ dom {y}, (f ran {y})⟩ ↔ x = y)))
66 xpdom.2 . . . . 5 𝐶 V
67 reldom 6162 . . . . . 6 Rel ≼
6867brrelexi 4327 . . . . 5 (ABA V)
69 xpexg 4395 . . . . 5 ((𝐶 V A V) → (𝐶 × A) V)
7066, 68, 69sylancr 393 . . . 4 (AB → (𝐶 × A) V)
7170adantr 261 . . 3 ((AB f:A1-1B) → (𝐶 × A) V)
7267brrelex2i 4328 . . . . 5 (ABB V)
73 xpexg 4395 . . . . 5 ((𝐶 V B V) → (𝐶 × B) V)
7466, 72, 73sylancr 393 . . . 4 (AB → (𝐶 × B) V)
7574adantr 261 . . 3 ((AB f:A1-1B) → (𝐶 × B) V)
7611, 65, 71, 75dom3d 6190 . 2 ((AB f:A1-1B) → (𝐶 × A) ≼ (𝐶 × B))
771, 76exlimddv 1775 1 (AB → (𝐶 × A) ≼ (𝐶 × B))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242   wcel 1390  wrex 2301  Vcvv 2551  {csn 3367  cop 3370   cuni 3571   class class class wbr 3755   × cxp 4286  dom cdm 4288  ran crn 4289  wf 4841  1-1wf1 4842  cfv 4845  cdom 6156
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fv 4853  df-dom 6159
This theorem is referenced by:  xpdom2g  6242
  Copyright terms: Public domain W3C validator