MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpdom2 Structured version   Visualization version   GIF version

Theorem xpdom2 8608
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 (𝐴𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))

Proof of Theorem xpdom2
Dummy variables 𝑢 𝑓 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdomi 8516 . 2 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
2 f1f 6565 . . . . . . . 8 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
3 ffvelrn 6840 . . . . . . . . 9 ((𝑓:𝐴𝐵 ran {𝑥} ∈ 𝐴) → (𝑓 ran {𝑥}) ∈ 𝐵)
43ex 416 . . . . . . . 8 (𝑓:𝐴𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
52, 4syl 17 . . . . . . 7 (𝑓:𝐴1-1𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
65anim2d 614 . . . . . 6 (𝑓:𝐴1-1𝐵 → (( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
76adantld 494 . . . . 5 (𝑓:𝐴1-1𝐵 → ((𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
8 elxp4 7622 . . . . 5 (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)))
9 opelxp 5578 . . . . 5 (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵) ↔ ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵))
107, 8, 93imtr4g 299 . . . 4 (𝑓:𝐴1-1𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
1110adantl 485 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
12 elxp2 5566 . . . . . 6 (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩)
13 elxp2 5566 . . . . . 6 (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩)
14 vex 3483 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
15 fvex 6674 . . . . . . . . . . . . . . . . . 18 (𝑓𝑤) ∈ V
1614, 15opth 5355 . . . . . . . . . . . . . . . . 17 (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)))
17 f1fveq 7012 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝐴1-1𝐵 ∧ (𝑤𝐴𝑢𝐴)) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
1817ancoms 462 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
1918anbi2d 631 . . . . . . . . . . . . . . . . 17 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)) ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2016, 19syl5bb 286 . . . . . . . . . . . . . . . 16 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2120ex 416 . . . . . . . . . . . . . . 15 ((𝑤𝐴𝑢𝐴) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2221ad2ant2l 745 . . . . . . . . . . . . . 14 (((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2322imp 410 . . . . . . . . . . . . 13 ((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2423adantlr 714 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
25 sneq 4560 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → {𝑥} = {⟨𝑧, 𝑤⟩})
2625dmeqd 5761 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
2726unieqd 4838 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
28 vex 3483 . . . . . . . . . . . . . . . . 17 𝑤 ∈ V
2914, 28op1sta 6069 . . . . . . . . . . . . . . . 16 dom {⟨𝑧, 𝑤⟩} = 𝑧
3027, 29syl6eq 2875 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = 𝑧)
3125rneqd 5795 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3231unieqd 4838 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3314, 28op2nda 6072 . . . . . . . . . . . . . . . . 17 ran {⟨𝑧, 𝑤⟩} = 𝑤
3432, 33syl6eq 2875 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = 𝑤)
3534fveq2d 6665 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑓 ran {𝑥}) = (𝑓𝑤))
3630, 35opeq12d 4797 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑧, 𝑤⟩ → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨𝑧, (𝑓𝑤)⟩)
37 sneq 4560 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → {𝑦} = {⟨𝑣, 𝑢⟩})
3837dmeqd 5761 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
3938unieqd 4838 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
40 vex 3483 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
41 vex 3483 . . . . . . . . . . . . . . . . 17 𝑢 ∈ V
4240, 41op1sta 6069 . . . . . . . . . . . . . . . 16 dom {⟨𝑣, 𝑢⟩} = 𝑣
4339, 42syl6eq 2875 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = 𝑣)
4437rneqd 5795 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4544unieqd 4838 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4640, 41op2nda 6072 . . . . . . . . . . . . . . . . 17 ran {⟨𝑣, 𝑢⟩} = 𝑢
4745, 46syl6eq 2875 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = 𝑢)
4847fveq2d 6665 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓 ran {𝑦}) = (𝑓𝑢))
4943, 48opeq12d 4797 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑣, 𝑢⟩ → ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ = ⟨𝑣, (𝑓𝑢)⟩)
5036, 49eqeqan12d 2841 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
5150ad2antlr 726 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
52 eqeq12 2838 . . . . . . . . . . . . . 14 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩))
5314, 28opth 5355 . . . . . . . . . . . . . 14 (⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))
5452, 53syl6bb 290 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5554ad2antlr 726 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5624, 51, 553bitr4d 314 . . . . . . . . . . 11 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))
5756exp53 451 . . . . . . . . . 10 ((𝑧𝐶𝑤𝐴) → ((𝑣𝐶𝑢𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
5857com23 86 . . . . . . . . 9 ((𝑧𝐶𝑤𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
5958rexlimivv 3284 . . . . . . . 8 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))
6059rexlimdvv 3285 . . . . . . 7 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → (∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))
6160imp 410 . . . . . 6 ((∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ ∧ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6212, 13, 61syl2anb 600 . . . . 5 ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6362com12 32 . . . 4 (𝑓:𝐴1-1𝐵 → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6463adantl 485 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
65 xpdom.2 . . . . 5 𝐶 ∈ V
66 reldom 8511 . . . . . 6 Rel ≼
6766brrelex1i 5595 . . . . 5 (𝐴𝐵𝐴 ∈ V)
68 xpexg 7467 . . . . 5 ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V)
6965, 67, 68sylancr 590 . . . 4 (𝐴𝐵 → (𝐶 × 𝐴) ∈ V)
7069adantr 484 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ∈ V)
7166brrelex2i 5596 . . . . 5 (𝐴𝐵𝐵 ∈ V)
72 xpexg 7467 . . . . 5 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V)
7365, 71, 72sylancr 590 . . . 4 (𝐴𝐵 → (𝐶 × 𝐵) ∈ V)
7473adantr 484 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐵) ∈ V)
7511, 64, 70, 74dom3d 8547 . 2 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
761, 75exlimddv 1937 1 (𝐴𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wrex 3134  Vcvv 3480  {csn 4550  cop 4556   cuni 4824   class class class wbr 5052   × cxp 5540  dom cdm 5542  ran crn 5543  wf 6339  1-1wf1 6340  cfv 6343  cdom 8503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fv 6351  df-dom 8507
This theorem is referenced by:  xpdom2g  8609  infxpenlem  9437  xpct  9440  djudom1  9606  cfpwsdom  10004  inar1  10195  rexpen  15581  2ndcctbss  22066  tx2ndc  22262  met2ndci  23135  mbfimaopnlem  24265
  Copyright terms: Public domain W3C validator