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

Theorem xpdom2 6769
 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 6687 . 2 (𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
2 f1f 5372 . . . . . . . 8 (𝑓:𝐴1-1𝐵𝑓:𝐴𝐵)
3 ffvelrn 5597 . . . . . . . . 9 ((𝑓:𝐴𝐵 ran {𝑥} ∈ 𝐴) → (𝑓 ran {𝑥}) ∈ 𝐵)
43ex 114 . . . . . . . 8 (𝑓:𝐴𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
52, 4syl 14 . . . . . . 7 (𝑓:𝐴1-1𝐵 → ( ran {𝑥} ∈ 𝐴 → (𝑓 ran {𝑥}) ∈ 𝐵))
65anim2d 335 . . . . . 6 (𝑓:𝐴1-1𝐵 → (( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
76adantld 276 . . . . 5 (𝑓:𝐴1-1𝐵 → ((𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)) → ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵)))
8 elxp4 5070 . . . . 5 (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = ⟨ dom {𝑥}, ran {𝑥}⟩ ∧ ( dom {𝑥} ∈ 𝐶 ran {𝑥} ∈ 𝐴)))
9 opelxp 4613 . . . . 5 (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵) ↔ ( dom {𝑥} ∈ 𝐶 ∧ (𝑓 ran {𝑥}) ∈ 𝐵))
107, 8, 93imtr4g 204 . . . 4 (𝑓:𝐴1-1𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
1110adantl 275 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ ∈ (𝐶 × 𝐵)))
12 elxp2 4601 . . . . . 6 (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩)
13 elxp2 4601 . . . . . 6 (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩)
14 vex 2715 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
15 vex 2715 . . . . . . . . . . . . . . . . . . 19 𝑓 ∈ V
16 vex 2715 . . . . . . . . . . . . . . . . . . 19 𝑤 ∈ V
1715, 16fvex 5485 . . . . . . . . . . . . . . . . . 18 (𝑓𝑤) ∈ V
1814, 17opth 4196 . . . . . . . . . . . . . . . . 17 (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)))
19 f1fveq 5717 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝐴1-1𝐵 ∧ (𝑤𝐴𝑢𝐴)) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
2019ancoms 266 . . . . . . . . . . . . . . . . . 18 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑓𝑤) = (𝑓𝑢) ↔ 𝑤 = 𝑢))
2120anbi2d 460 . . . . . . . . . . . . . . . . 17 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → ((𝑧 = 𝑣 ∧ (𝑓𝑤) = (𝑓𝑢)) ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2218, 21syl5bb 191 . . . . . . . . . . . . . . . 16 (((𝑤𝐴𝑢𝐴) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2322ex 114 . . . . . . . . . . . . . . 15 ((𝑤𝐴𝑢𝐴) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2423ad2ant2l 500 . . . . . . . . . . . . . 14 (((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))))
2524imp 123 . . . . . . . . . . . . 13 ((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
2625adantlr 469 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
27 sneq 3571 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → {𝑥} = {⟨𝑧, 𝑤⟩})
2827dmeqd 4785 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
2928unieqd 3783 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩})
3014, 16op1sta 5064 . . . . . . . . . . . . . . . 16 dom {⟨𝑧, 𝑤⟩} = 𝑧
3129, 30eqtrdi 2206 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = 𝑧)
3227rneqd 4812 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3332unieqd 3783 . . . . . . . . . . . . . . . . 17 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩})
3414, 16op2nda 5067 . . . . . . . . . . . . . . . . 17 ran {⟨𝑧, 𝑤⟩} = 𝑤
3533, 34eqtrdi 2206 . . . . . . . . . . . . . . . 16 (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = 𝑤)
3635fveq2d 5469 . . . . . . . . . . . . . . 15 (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑓 ran {𝑥}) = (𝑓𝑤))
3731, 36opeq12d 3749 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑧, 𝑤⟩ → ⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨𝑧, (𝑓𝑤)⟩)
38 sneq 3571 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → {𝑦} = {⟨𝑣, 𝑢⟩})
3938dmeqd 4785 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
4039unieqd 3783 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩})
41 vex 2715 . . . . . . . . . . . . . . . . 17 𝑣 ∈ V
42 vex 2715 . . . . . . . . . . . . . . . . 17 𝑢 ∈ V
4341, 42op1sta 5064 . . . . . . . . . . . . . . . 16 dom {⟨𝑣, 𝑢⟩} = 𝑣
4440, 43eqtrdi 2206 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = 𝑣)
4538rneqd 4812 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4645unieqd 3783 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩})
4741, 42op2nda 5067 . . . . . . . . . . . . . . . . 17 ran {⟨𝑣, 𝑢⟩} = 𝑢
4846, 47eqtrdi 2206 . . . . . . . . . . . . . . . 16 (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = 𝑢)
4948fveq2d 5469 . . . . . . . . . . . . . . 15 (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓 ran {𝑦}) = (𝑓𝑢))
5044, 49opeq12d 3749 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑣, 𝑢⟩ → ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ = ⟨𝑣, (𝑓𝑢)⟩)
5137, 50eqeqan12d 2173 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
5251ad2antlr 481 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓𝑤)⟩ = ⟨𝑣, (𝑓𝑢)⟩))
53 eqeq12 2170 . . . . . . . . . . . . . 14 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩))
5414, 16opth 4196 . . . . . . . . . . . . . 14 (⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩ ↔ (𝑧 = 𝑣𝑤 = 𝑢))
5553, 54bitrdi 195 . . . . . . . . . . . . 13 ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5655ad2antlr 481 . . . . . . . . . . . 12 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣𝑤 = 𝑢)))
5726, 52, 563bitr4d 219 . . . . . . . . . . 11 (((((𝑧𝐶𝑤𝐴) ∧ (𝑣𝐶𝑢𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴1-1𝐵) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))
5857exp53 375 . . . . . . . . . 10 ((𝑧𝐶𝑤𝐴) → ((𝑣𝐶𝑢𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
5958com23 78 . . . . . . . . 9 ((𝑧𝐶𝑤𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))))
6059rexlimivv 2580 . . . . . . . 8 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣𝐶𝑢𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))
6160rexlimdvv 2581 . . . . . . 7 (∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → (∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))
6261imp 123 . . . . . 6 ((∃𝑧𝐶𝑤𝐴 𝑥 = ⟨𝑧, 𝑤⟩ ∧ ∃𝑣𝐶𝑢𝐴 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6312, 13, 62syl2anb 289 . . . . 5 ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (𝑓:𝐴1-1𝐵 → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6463com12 30 . . . 4 (𝑓:𝐴1-1𝐵 → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
6564adantl 275 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨ dom {𝑥}, (𝑓 ran {𝑥})⟩ = ⟨ dom {𝑦}, (𝑓 ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))
66 xpdom.2 . . . . 5 𝐶 ∈ V
67 reldom 6683 . . . . . 6 Rel ≼
6867brrelex1i 4626 . . . . 5 (𝐴𝐵𝐴 ∈ V)
69 xpexg 4697 . . . . 5 ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V)
7066, 68, 69sylancr 411 . . . 4 (𝐴𝐵 → (𝐶 × 𝐴) ∈ V)
7170adantr 274 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ∈ V)
7267brrelex2i 4627 . . . . 5 (𝐴𝐵𝐵 ∈ V)
73 xpexg 4697 . . . . 5 ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V)
7466, 72, 73sylancr 411 . . . 4 (𝐴𝐵 → (𝐶 × 𝐵) ∈ V)
7574adantr 274 . . 3 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐵) ∈ V)
7611, 65, 71, 75dom3d 6712 . 2 ((𝐴𝐵𝑓:𝐴1-1𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
771, 76exlimddv 1878 1 (𝐴𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1335   ∈ wcel 2128  ∃wrex 2436  Vcvv 2712  {csn 3560  ⟨cop 3563  ∪ cuni 3772   class class class wbr 3965   × cxp 4581  dom cdm 4583  ran crn 4584  ⟶wf 5163  –1-1→wf1 5164  ‘cfv 5167   ≼ cdom 6677 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168  ax-un 4392 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4252  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fv 5175  df-dom 6680 This theorem is referenced by:  xpdom2g  6770  xpct  12097
 Copyright terms: Public domain W3C validator