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

Theorem xpdom2 6335
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 6260 . 2 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
2 f1f 5119 . . . . . . . 8 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
3 ffvelrn 5327 . . . . . . . . 9 ((𝑓:𝐴𝐵 ran {𝑥} ∈ 𝐴) → (𝑓 ran {𝑥}) ∈ 𝐵)
43ex 112 . . . . . . . 8 (𝑓:𝐴𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
52, 4syl 14 . . . . . . 7 (𝑓:𝐴1-1𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
65anim2d 324 . . . . . 6 (𝑓:𝐴1-1𝐵 → (( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
76adantld 267 . . . . 5 (𝑓:𝐴1-1𝐵 → ((𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
8 elxp4 4835 . . . . 5 (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)))
9 opelxp 4401 . . . . 5 (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵) ↔ ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵))
107, 8, 93imtr4g 198 . . . 4 (𝑓:𝐴1-1𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
1110adantl 266 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
12 elxp2 4390 . . . . . 6 (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩)
13 elxp2 4390 . . . . . 6 (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩)
14 vex 2577 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
15 vex 2577 . . . . . . . . . . . . . . . . . . 19 𝑓 ∈ V
16 vex 2577 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ V
1715, 16fvex 5222 . . . . . . . . . . . . . . . . . 18 (𝑓𝑤) ∈ V
1814, 17opth 4001 . . . . . . . . . . . . . . . . 17 (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)))
19 f1fveq 5438 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝐴1-1𝐵 ∧ (𝑤𝐴𝑢𝐴)) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
2019ancoms 259 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
2120anbi2d 445 . . . . . . . . . . . . . . . . 17 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)) ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2218, 21syl5bb 185 . . . . . . . . . . . . . . . 16 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2322ex 112 . . . . . . . . . . . . . . 15 ((𝑤𝐴𝑢𝐴) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2423ad2ant2l 485 . . . . . . . . . . . . . 14 (((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2524imp 119 . . . . . . . . . . . . 13 ((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2625adantlr 454 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
27 sneq 3413 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → {𝑥} = {⟨𝑧, 𝑤⟩})
2827dmeqd 4564 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
2928unieqd 3618 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
3014, 16op1sta 4829 . . . . . . . . . . . . . . . 16 dom {⟨𝑧, 𝑤⟩} = 𝑧
3129, 30syl6eq 2104 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = 𝑧)
3227rneqd 4590 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3332unieqd 3618 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3414, 16op2nda 4832 . . . . . . . . . . . . . . . . 17 ran {⟨𝑧, 𝑤⟩} = 𝑤
3533, 34syl6eq 2104 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = 𝑤)
3635fveq2d 5209 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑓 ran {𝑥}) = (𝑓𝑤))
3731, 36opeq12d 3584 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑧, 𝑤⟩ → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨𝑧, (𝑓𝑤)⟩)
38 sneq 3413 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → {𝑦} = {⟨𝑣, 𝑢⟩})
3938dmeqd 4564 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
4039unieqd 3618 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
41 vex 2577 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
42 vex 2577 . . . . . . . . . . . . . . . . 17 𝑢 ∈ V
4341, 42op1sta 4829 . . . . . . . . . . . . . . . 16 dom {⟨𝑣, 𝑢⟩} = 𝑣
4440, 43syl6eq 2104 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = 𝑣)
4538rneqd 4590 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4645unieqd 3618 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4741, 42op2nda 4832 . . . . . . . . . . . . . . . . 17 ran {⟨𝑣, 𝑢⟩} = 𝑢
4846, 47syl6eq 2104 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = 𝑢)
4948fveq2d 5209 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓 ran {𝑦}) = (𝑓𝑢))
5044, 49opeq12d 3584 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑣, 𝑢⟩ → ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ = ⟨𝑣, (𝑓𝑢)⟩)
5137, 50eqeqan12d 2071 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
5251ad2antlr 466 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
53 eqeq12 2068 . . . . . . . . . . . . . 14 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩))
5414, 16opth 4001 . . . . . . . . . . . . . 14 (⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))
5553, 54syl6bb 189 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5655ad2antlr 466 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5726, 52, 563bitr4d 213 . . . . . . . . . . 11 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))
5857exp53 363 . . . . . . . . . 10 ((𝑧𝐶𝑤𝐴) → ((𝑣𝐶𝑢𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
5958com23 76 . . . . . . . . 9 ((𝑧𝐶𝑤𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
6059rexlimivv 2455 . . . . . . . 8 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))
6160rexlimdvv 2456 . . . . . . 7 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → (∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))
6261imp 119 . . . . . 6 ((∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ ∧ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6312, 13, 62syl2anb 279 . . . . 5 ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6463com12 30 . . . 4 (𝑓:𝐴1-1𝐵 → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6564adantl 266 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
66 xpdom.2 . . . . 5 𝐶 ∈ V
67 reldom 6256 . . . . . 6 Rel ≼
6867brrelexi 4411 . . . . 5 (𝐴𝐵𝐴 ∈ V)
69 xpexg 4479 . . . . 5 ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V)
7066, 68, 69sylancr 399 . . . 4 (𝐴𝐵 → (𝐶 × 𝐴) ∈ V)
7170adantr 265 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ∈ V)
7267brrelex2i 4412 . . . . 5 (𝐴𝐵𝐵 ∈ V)
73 xpexg 4479 . . . . 5 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V)
7466, 72, 73sylancr 399 . . . 4 (𝐴𝐵 → (𝐶 × 𝐵) ∈ V)
7574adantr 265 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐵) ∈ V)
7611, 65, 71, 75dom3d 6284 . 2 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
771, 76exlimddv 1794 1 (𝐴𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102   = wceq 1259  wcel 1409  wrex 2324  Vcvv 2574  {csn 3402  cop 3405   cuni 3607   class class class wbr 3791   × cxp 4370  dom cdm 4372  ran crn 4373  wf 4925  1-1wf1 4926  cfv 4929  cdom 6250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-un 4197
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-mpt 3847  df-id 4057  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fv 4937  df-dom 6253
This theorem is referenced by:  xpdom2g  6336
  Copyright terms: Public domain W3C validator