Theorem xpdom2 3345

Description: Dominance law for cross product. Proposition 10.33(2) of [TakeutiZaring] p. 92.

Hypotheses

Ref	Expression
xpdom2.1	⊢ A ∈ V
xpdom2.2	⊢ B ∈ V
xpdom2.3	⊢ C ∈ V

Assertion

Ref	Expression
xpdom2	⊢ (A ≼ B → (C × A) ≼ (C × B))

Proof of Theorem xpdom2

Step	Hyp	Ref	Expression
1		xpdom2.2	. . 3 ⊢ B ∈ V
2	1	brdom 3283	. 2 ⊢ (A ≼ B ↔ ∃f f:A–1-1→B)
3		xpdom2.3	. . . . 5 ⊢ C ∈ V
4		xpdom2.1	. . . . 5 ⊢ A ∈ V
5	3, 4	xpex 2488	. . . 4 ⊢ (C × A) ∈ V
6		f1f 2781	. . . . . . . . 9 ⊢ (f:A–1-1→B → f:A–→B)
7		ffvrn 2890	. . . . . . . . . 10 ⊢ ((f:A–→B ∧ ∪ran {x} ∈ A) → (f ‘∪ran {x}) ∈ B)
8	7	exp 291	. . . . . . . . 9 ⊢ (f:A–→B → (∪ran {x} ∈ A → (f ‘∪ran {x}) ∈ B))
9	6, 8	syl 12	. . . . . . . 8 ⊢ (f:A–1-1→B → (∪ran {x} ∈ A → (f ‘∪ran {x}) ∈ B))
10	9	anim2d 433	. . . . . . 7 ⊢ (f:A–1-1→B → ((∪dom {x} ∈ C ∧ ∪ran {x} ∈ A) → (∪dom {x} ∈ C ∧ (f ‘∪ran {x}) ∈ B)))
11	10	adantld 307	. . . . . 6 ⊢ (f:A–1-1→B → ((x = ⟨∪dom {x}, ∪ran {x}⟩ ∧ (∪dom {x} ∈ C ∧ ∪ran {x} ∈ A)) → (∪dom {x} ∈ C ∧ (f ‘∪ran {x}) ∈ B)))
12		elxp4 2640	. . . . . 6 ⊢ (x ∈ (C × A) ↔ (x = ⟨∪dom {x}, ∪ran {x}⟩ ∧ (∪dom {x} ∈ C ∧ ∪ran {x} ∈ A)))
13		fvex 2838	. . . . . . 7 ⊢ (f ‘∪ran {x}) ∈ V
14	13	opelxp 2452	. . . . . 6 ⊢ (⟨∪dom {x}, (f ‘∪ran {x})⟩ ∈ (C × B) ↔ (∪dom {x} ∈ C ∧ (f ‘∪ran {x}) ∈ B))
15	11, 12, 14	3imtr4g 426	. . . . 5 ⊢ (f:A–1-1→B → (x ∈ (C × A) → ⟨∪dom {x}, (f ‘∪ran {x})⟩ ∈ (C × B)))
16		sneq 1816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = ⟨z, w⟩ → {x} = {⟨z, w⟩})
17	16	dmeqd 2533	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = ⟨z, w⟩ → dom {x} = dom {⟨z, w⟩})
18	17	unieqd 1929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = ⟨z, w⟩ → ∪dom {x} = ∪dom {⟨z, w⟩})
19		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ z ∈ V
20	19	op1sta 2635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪dom {⟨z, w⟩} = z
21	18, 20	syl6eq 1140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = ⟨z, w⟩ → ∪dom {x} = z)
22	16	rneqd 2557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = ⟨z, w⟩ → ran {x} = ran {⟨z, w⟩})
23	22	unieqd 1929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = ⟨z, w⟩ → ∪ran {x} = ∪ran {⟨z, w⟩})
24		visset 1350	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ w ∈ V
25	19, 24	op2nda 2639	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ran {⟨z, w⟩} = w
26	23, 25	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = ⟨z, w⟩ → ∪ran {x} = w)
27	26	fveq2d 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = ⟨z, w⟩ → (f ‘∪ran {x}) = (f ‘w))
28	21, 27	jca 236	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = ⟨z, w⟩ → (∪dom {x} = z ∧ (f ‘∪ran {x}) = (f ‘w)))
29		snex 1859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {x} ∈ V
30		dmexg 2551	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({x} ∈ V → dom {x} ∈ V)
31	29, 30	ax-mp 6	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom {x} ∈ V
32	31	uniex 1947	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪dom {x} ∈ V
33		fvex 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f ‘w) ∈ V
34	32, 13, 33	opth 1898	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨z, (f ‘w)⟩ ↔ (∪dom {x} = z ∧ (f ‘∪ran {x}) = (f ‘w)))
35	28, 34	sylibr 175	. . . . . . . . . . . . . . . . . 18 ⊢ (x = ⟨z, w⟩ → ⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨z, (f ‘w)⟩)
36		sneq 1816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y = ⟨v, u⟩ → {y} = {⟨v, u⟩})
37	36	dmeqd 2533	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = ⟨v, u⟩ → dom {y} = dom {⟨v, u⟩})
38	37	unieqd 1929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = ⟨v, u⟩ → ∪dom {y} = ∪dom {⟨v, u⟩})
39		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ v ∈ V
40	39	op1sta 2635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪dom {⟨v, u⟩} = v
41	38, 40	syl6eq 1140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = ⟨v, u⟩ → ∪dom {y} = v)
42	36	rneqd 2557	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y = ⟨v, u⟩ → ran {y} = ran {⟨v, u⟩})
43	42	unieqd 1929	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = ⟨v, u⟩ → ∪ran {y} = ∪ran {⟨v, u⟩})
44		visset 1350	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ u ∈ V
45	39, 44	op2nda 2639	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ran {⟨v, u⟩} = u
46	43, 45	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = ⟨v, u⟩ → ∪ran {y} = u)
47	46	fveq2d 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = ⟨v, u⟩ → (f ‘∪ran {y}) = (f ‘u))
48	41, 47	jca 236	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = ⟨v, u⟩ → (∪dom {y} = v ∧ (f ‘∪ran {y}) = (f ‘u)))
49		snex 1859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {y} ∈ V
50		dmexg 2551	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({y} ∈ V → dom {y} ∈ V)
51	49, 50	ax-mp 6	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom {y} ∈ V
52	51	uniex 1947	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪dom {y} ∈ V
53		fvex 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f ‘∪ran {y}) ∈ V
54		fvex 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f ‘u) ∈ V
55	52, 53, 54	opth 1898	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨∪dom {y}, (f ‘∪ran {y})⟩ = ⟨v, (f ‘u)⟩ ↔ (∪dom {y} = v ∧ (f ‘∪ran {y}) = (f ‘u)))
56	48, 55	sylibr 175	. . . . . . . . . . . . . . . . . 18 ⊢ (y = ⟨v, u⟩ → ⟨∪dom {y}, (f ‘∪ran {y})⟩ = ⟨v, (f ‘u)⟩)
57	35, 56	cleqan12d 1116	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ ⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩))
58	57	adantl 305	. . . . . . . . . . . . . . . 16 ⊢ ((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ ⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩))
59	58	adantr 306	. . . . . . . . . . . . . . 15 ⊢ (((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) ∧ f:A–1-1→B) → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ ⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩))
60		f1fveq 2918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f:A–1-1→B ∧ (w ∈ A ∧ u ∈ A)) → ((f ‘w) = (f ‘u) ↔ w = u))
61	60	ancoms 334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((w ∈ A ∧ u ∈ A) ∧ f:A–1-1→B) → ((f ‘w) = (f ‘u) ↔ w = u))
62	61	anbi2d 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((w ∈ A ∧ u ∈ A) ∧ f:A–1-1→B) → ((z = v ∧ (f ‘w) = (f ‘u)) ↔ (z = v ∧ w = u)))
63	19, 33, 54	opth 1898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ∧ (f ‘w) = (f ‘u)))
64	62, 63	syl5bb 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((w ∈ A ∧ u ∈ A) ∧ f:A–1-1→B) → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ∧ w = u)))
65	64	exp 291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((w ∈ A ∧ u ∈ A) → (f:A–1-1→B → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ∧ w = u))))
66	65	adantrl 311	. . . . . . . . . . . . . . . . . 18 ⊢ ((w ∈ A ∧ (v ∈ C ∧ u ∈ A)) → (f:A–1-1→B → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ∧ w = u))))
67	66	adantll 309	. . . . . . . . . . . . . . . . 17 ⊢ (((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) → (f:A–1-1→B → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ∧ w = u))))
68	67	imp 277	. . . . . . . . . . . . . . . 16 ⊢ ((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ f:A–1-1→B) → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ∧ w = u)))
69	68	adantlr 310	. . . . . . . . . . . . . . 15 ⊢ (((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) ∧ f:A–1-1→B) → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ∧ w = u)))
70	59, 69	bitrd 406	. . . . . . . . . . . . . 14 ⊢ (((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) ∧ f:A–1-1→B) → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ (z = v ∧ w = u)))
71		cleq12 1113	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) → (x = y ↔ ⟨z, w⟩ = ⟨v, u⟩))
72	19, 24, 44	opth 1898	. . . . . . . . . . . . . . . . 17 ⊢ (⟨z, w⟩ = ⟨v, u⟩ ↔ (z = v ∧ w = u))
73	71, 72	syl6bb 414	. . . . . . . . . . . . . . . 16 ⊢ ((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) → (x = y ↔ (z = v ∧ w = u)))
74	73	adantl 305	. . . . . . . . . . . . . . 15 ⊢ ((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) → (x = y ↔ (z = v ∧ w = u)))
75	74	adantr 306	. . . . . . . . . . . . . 14 ⊢ (((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) ∧ f:A–1-1→B) → (x = y ↔ (z = v ∧ w = u)))
76	70, 75	bitr4d 409	. . . . . . . . . . . . 13 ⊢ (((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) ∧ f:A–1-1→B) → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y))
77	76	exp 291	. . . . . . . . . . . 12 ⊢ ((((z ∈ C ∧ w ∈ A) ∧ (v ∈ C ∧ u ∈ A)) ∧ (x = ⟨z, w⟩ ∧ y = ⟨v, u⟩)) → (f:A–1-1→B → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y)))
78	77	exp43 301	. . . . . . . . . . 11 ⊢ ((z ∈ C ∧ w ∈ A) → ((v ∈ C ∧ u ∈ A) → (x = ⟨z, w⟩ → (y = ⟨v, u⟩ → (f:A–1-1→B → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y))))))
79	78	com23 32	. . . . . . . . . 10 ⊢ ((z ∈ C ∧ w ∈ A) → (x = ⟨z, w⟩ → ((v ∈ C ∧ u ∈ A) → (y = ⟨v, u⟩ → (f:A–1-1→B → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y))))))
80	79	r19.23aivv 1287	. . . . . . . . 9 ⊢ (∃z ∈ C ∃w ∈ A x = ⟨z, w⟩ → ((v ∈ C ∧ u ∈ A) → (y = ⟨v, u⟩ → (f:A–1-1→B → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y)))))
81	80	r19.23advv 1288	. . . . . . . 8 ⊢ (∃z ∈ C ∃w ∈ A x = ⟨z, w⟩ → (∃v ∈ C ∃u ∈ A y = ⟨v, u⟩ → (f:A–1-1→B → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y))))
82	81	imp 277	. . . . . . 7 ⊢ ((∃z ∈ C ∃w ∈ A x = ⟨z, w⟩ ∧ ∃v ∈ C ∃u ∈ A y = ⟨v, u⟩) → (f:A–1-1→B → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y)))
83		elxp2 2443	. . . . . . 7 ⊢ (x ∈ (C × A) ↔ ∃z ∈ C ∃w ∈ A x = ⟨z, w⟩)
84		elxp2 2443	. . . . . . 7 ⊢ (y ∈ (C × A) ↔ ∃v ∈ C ∃u ∈ A y = ⟨v, u⟩)
85	82, 83, 84	syl2anb 350	. . . . . 6 ⊢ ((x ∈ (C × A) ∧ y ∈ (C × A)) → (f:A–1-1→B → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y)))
86	85	com12 13	. . . . 5 ⊢ (f:A–1-1→B → ((x ∈ (C × A) ∧ y ∈ (C × A)) → (⟨∪dom {x}, (f ‘∪ran {x})⟩ = ⟨∪dom {y}, (f ‘∪ran {y})⟩ ↔ x = y)))
87	15, 86	dom2d 3307	. . . 4 ⊢ (f:A–1-1→B → ((C × A) ∈ V → (C × A) ≼ (C × B)))
88	5, 87	mpi 44	. . 3 ⊢ (f:A–1-1→B → (C × A) ≼ (C × B))
89	88	19.23aiv 952	. 2 ⊢ (∃f f:A–1-1→B → (C × A) ≼ (C × B))
90	2, 89	sylbi 174	1 ⊢ (A ≼ B → (C × A) ≼ (C × B))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   = weq 797   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348  {csn 1808  ⟨cop 1810  ∪cuni 1919   class class class wbr 2054   × cxp 2408  dom cdm 2410  ran crn 2411  –→wf 2418  –1-1→wf1 2419   ‘cfv 2422   ≼ cdom 3272

This theorem is referenced by:  xpdom1 3346  xpen 3383  infunabs 4946  infcdaabs 4947  infxpabs 4949

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-en 3274  df-dom 3275

metamath.org