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

Theorem xpdom2 9067
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 8954 . 2 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
2 f1f 6788 . . . . . . . 8 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
3 ffvelcdm 7084 . . . . . . . . 9 ((𝑓:𝐴𝐵 ran {𝑥} ∈ 𝐴) → (𝑓 ran {𝑥}) ∈ 𝐵)
43ex 414 . . . . . . . 8 (𝑓:𝐴𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
52, 4syl 17 . . . . . . 7 (𝑓:𝐴1-1𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
65anim2d 613 . . . . . 6 (𝑓:𝐴1-1𝐵 → (( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
76adantld 492 . . . . 5 (𝑓:𝐴1-1𝐵 → ((𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
8 elxp4 7913 . . . . 5 (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)))
9 opelxp 5713 . . . . 5 (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵) ↔ ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵))
107, 8, 93imtr4g 296 . . . 4 (𝑓:𝐴1-1𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
1110adantl 483 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
12 elxp2 5701 . . . . . 6 (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩)
13 elxp2 5701 . . . . . 6 (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩)
14 vex 3479 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
15 fvex 6905 . . . . . . . . . . . . . . . . . 18 (𝑓𝑤) ∈ V
1614, 15opth 5477 . . . . . . . . . . . . . . . . 17 (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)))
17 f1fveq 7261 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝐴1-1𝐵 ∧ (𝑤𝐴𝑢𝐴)) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
1817ancoms 460 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
1918anbi2d 630 . . . . . . . . . . . . . . . . 17 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)) ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2016, 19bitrid 283 . . . . . . . . . . . . . . . 16 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2120ex 414 . . . . . . . . . . . . . . 15 ((𝑤𝐴𝑢𝐴) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2221ad2ant2l 745 . . . . . . . . . . . . . 14 (((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2322imp 408 . . . . . . . . . . . . 13 ((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2423adantlr 714 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
25 sneq 4639 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → {𝑥} = {⟨𝑧, 𝑤⟩})
2625dmeqd 5906 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
2726unieqd 4923 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
28 vex 3479 . . . . . . . . . . . . . . . . 17 𝑤 ∈ V
2914, 28op1sta 6225 . . . . . . . . . . . . . . . 16 dom {⟨𝑧, 𝑤⟩} = 𝑧
3027, 29eqtrdi 2789 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = 𝑧)
3125rneqd 5938 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3231unieqd 4923 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3314, 28op2nda 6228 . . . . . . . . . . . . . . . . 17 ran {⟨𝑧, 𝑤⟩} = 𝑤
3432, 33eqtrdi 2789 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = 𝑤)
3534fveq2d 6896 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑓 ran {𝑥}) = (𝑓𝑤))
3630, 35opeq12d 4882 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑧, 𝑤⟩ → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨𝑧, (𝑓𝑤)⟩)
37 sneq 4639 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → {𝑦} = {⟨𝑣, 𝑢⟩})
3837dmeqd 5906 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
3938unieqd 4923 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
40 vex 3479 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
41 vex 3479 . . . . . . . . . . . . . . . . 17 𝑢 ∈ V
4240, 41op1sta 6225 . . . . . . . . . . . . . . . 16 dom {⟨𝑣, 𝑢⟩} = 𝑣
4339, 42eqtrdi 2789 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = 𝑣)
4437rneqd 5938 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4544unieqd 4923 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4640, 41op2nda 6228 . . . . . . . . . . . . . . . . 17 ran {⟨𝑣, 𝑢⟩} = 𝑢
4745, 46eqtrdi 2789 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = 𝑢)
4847fveq2d 6896 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓 ran {𝑦}) = (𝑓𝑢))
4943, 48opeq12d 4882 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑣, 𝑢⟩ → ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ = ⟨𝑣, (𝑓𝑢)⟩)
5036, 49eqeqan12d 2747 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
5150ad2antlr 726 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
52 eqeq12 2750 . . . . . . . . . . . . . 14 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩))
5314, 28opth 5477 . . . . . . . . . . . . . 14 (⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))
5452, 53bitrdi 287 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5554ad2antlr 726 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5624, 51, 553bitr4d 311 . . . . . . . . . . 11 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))
5756exp53 449 . . . . . . . . . 10 ((𝑧𝐶𝑤𝐴) → ((𝑣𝐶𝑢𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
5857com23 86 . . . . . . . . 9 ((𝑧𝐶𝑤𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
5958rexlimivv 3200 . . . . . . . 8 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))
6059rexlimdvv 3211 . . . . . . 7 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → (∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))
6160imp 408 . . . . . 6 ((∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ ∧ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6212, 13, 61syl2anb 599 . . . . 5 ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6362com12 32 . . . 4 (𝑓:𝐴1-1𝐵 → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6463adantl 483 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
65 xpdom.2 . . . . 5 𝐶 ∈ V
66 reldom 8945 . . . . . 6 Rel ≼
6766brrelex1i 5733 . . . . 5 (𝐴𝐵𝐴 ∈ V)
68 xpexg 7737 . . . . 5 ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V)
6965, 67, 68sylancr 588 . . . 4 (𝐴𝐵 → (𝐶 × 𝐴) ∈ V)
7069adantr 482 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ∈ V)
7166brrelex2i 5734 . . . . 5 (𝐴𝐵𝐵 ∈ V)
72 xpexg 7737 . . . . 5 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V)
7365, 71, 72sylancr 588 . . . 4 (𝐴𝐵 → (𝐶 × 𝐵) ∈ V)
7473adantr 482 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐵) ∈ V)
7511, 64, 70, 74dom3d 8990 . 2 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
761, 75exlimddv 1939 1 (𝐴𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wrex 3071  Vcvv 3475  {csn 4629  cop 4635   cuni 4909   class class class wbr 5149   × cxp 5675  dom cdm 5677  ran crn 5678  wf 6540  1-1wf1 6541  cfv 6544  cdom 8937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fv 6552  df-dom 8941
This theorem is referenced by:  xpdom2g  9068  infxpenlem  10008  xpct  10011  djudom1  10177  cfpwsdom  10579  inar1  10770  rexpen  16171  2ndcctbss  22959  tx2ndc  23155  met2ndci  24031  mbfimaopnlem  25172
  Copyright terms: Public domain W3C validator