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

Theorem xpdom2 8941
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 8828 . 2 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
2 f1f 6730 . . . . . . . 8 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
3 ffvelcdm 7024 . . . . . . . . 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 7846 . . . . 5 (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)))
9 opelxp 5663 . . . . 5 (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵) ↔ ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵))
107, 8, 93imtr4g 296 . . . 4 (𝑓:𝐴1-1𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
1110adantl 483 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
12 elxp2 5651 . . . . . 6 (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩)
13 elxp2 5651 . . . . . 6 (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩)
14 vex 3447 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
15 fvex 6847 . . . . . . . . . . . . . . . . . 18 (𝑓𝑤) ∈ V
1614, 15opth 5428 . . . . . . . . . . . . . . . . 17 (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)))
17 f1fveq 7200 . . . . . . . . . . . . . . . . . . 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 744 . . . . . . . . . . . . . 14 (((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2322imp 408 . . . . . . . . . . . . 13 ((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2423adantlr 713 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
25 sneq 4591 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → {𝑥} = {⟨𝑧, 𝑤⟩})
2625dmeqd 5854 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
2726unieqd 4874 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
28 vex 3447 . . . . . . . . . . . . . . . . 17 𝑤 ∈ V
2914, 28op1sta 6170 . . . . . . . . . . . . . . . 16 dom {⟨𝑧, 𝑤⟩} = 𝑧
3027, 29eqtrdi 2793 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = 𝑧)
3125rneqd 5886 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3231unieqd 4874 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3314, 28op2nda 6173 . . . . . . . . . . . . . . . . 17 ran {⟨𝑧, 𝑤⟩} = 𝑤
3432, 33eqtrdi 2793 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = 𝑤)
3534fveq2d 6838 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑓 ran {𝑥}) = (𝑓𝑤))
3630, 35opeq12d 4833 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑧, 𝑤⟩ → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨𝑧, (𝑓𝑤)⟩)
37 sneq 4591 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → {𝑦} = {⟨𝑣, 𝑢⟩})
3837dmeqd 5854 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
3938unieqd 4874 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
40 vex 3447 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
41 vex 3447 . . . . . . . . . . . . . . . . 17 𝑢 ∈ V
4240, 41op1sta 6170 . . . . . . . . . . . . . . . 16 dom {⟨𝑣, 𝑢⟩} = 𝑣
4339, 42eqtrdi 2793 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = 𝑣)
4437rneqd 5886 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4544unieqd 4874 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4640, 41op2nda 6173 . . . . . . . . . . . . . . . . 17 ran {⟨𝑣, 𝑢⟩} = 𝑢
4745, 46eqtrdi 2793 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = 𝑢)
4847fveq2d 6838 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓 ran {𝑦}) = (𝑓𝑢))
4943, 48opeq12d 4833 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑣, 𝑢⟩ → ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ = ⟨𝑣, (𝑓𝑢)⟩)
5036, 49eqeqan12d 2751 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
5150ad2antlr 725 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
52 eqeq12 2754 . . . . . . . . . . . . . 14 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩))
5314, 28opth 5428 . . . . . . . . . . . . . 14 (⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))
5452, 53bitrdi 287 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5554ad2antlr 725 . . . . . . . . . . . 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 3194 . . . . . . . 8 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))
6059rexlimdvv 3202 . . . . . . 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 8819 . . . . . 6 Rel ≼
6766brrelex1i 5681 . . . . 5 (𝐴𝐵𝐴 ∈ V)
68 xpexg 7671 . . . . 5 ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V)
6965, 67, 68sylancr 588 . . . 4 (𝐴𝐵 → (𝐶 × 𝐴) ∈ V)
7069adantr 482 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ∈ V)
7166brrelex2i 5682 . . . . 5 (𝐴𝐵𝐵 ∈ V)
72 xpexg 7671 . . . . 5 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V)
7365, 71, 72sylancr 588 . . . 4 (𝐴𝐵 → (𝐶 × 𝐵) ∈ V)
7473adantr 482 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐵) ∈ V)
7511, 64, 70, 74dom3d 8864 . 2 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
761, 75exlimddv 1938 1 (𝐴𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1541  wcel 2106  wrex 3071  Vcvv 3443  {csn 4581  cop 4587   cuni 4860   class class class wbr 5100   × cxp 5625  dom cdm 5627  ran crn 5628  wf 6484  1-1wf1 6485  cfv 6488  cdom 8811
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-br 5101  df-opab 5163  df-mpt 5184  df-id 5525  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fv 6496  df-dom 8815
This theorem is referenced by:  xpdom2g  8942  infxpenlem  9879  xpct  9882  djudom1  10048  cfpwsdom  10450  inar1  10641  rexpen  16041  2ndcctbss  22716  tx2ndc  22912  met2ndci  23788  mbfimaopnlem  24929
  Copyright terms: Public domain W3C validator