Theorem xpdom2 4448

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

Hypotheses

Ref	Expression
xpdom.1	⊢ B ∈ V
xpdom.2	⊢ C ∈ V

Assertion

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

Proof of Theorem xpdom2

Step	Hyp	Ref	Expression
1		reldom 4379	. . 3 ⊢ Rel ≼
2	1	brrelexi 3214	. 2 ⊢ (A ≼ B → A ∈ V)
3		breq1 2627	. . . 4 ⊢ (t = A → (t ≼ B ↔ A ≼ B))
4		xpeq2 3207	. . . . 5 ⊢ (t = A → (C × t) = (C × A))
5	4	breq1d 2634	. . . 4 ⊢ (t = A → ((C × t) ≼ (C × B) ↔ (C × A) ≼ (C × B)))
6	3, 5	imbi12d 628	. . 3 ⊢ (t = A → ((t ≼ B → (C × t) ≼ (C × B)) ↔ (A ≼ B → (C × A) ≼ (C × B))))
7		xpdom.1	. . . . 5 ⊢ B ∈ V
8	7	brdom 4384	. . . 4 ⊢ (t ≼ B ↔ ∃f f:t–1-1→B)
9		xpdom.2	. . . . . . 7 ⊢ C ∈ V
10		visset 1816	. . . . . . 7 ⊢ t ∈ V
11	9, 10	xpex 3266	. . . . . 6 ⊢ (C × t) ∈ V
12		f1f 3671	. . . . . . . . . . 11 ⊢ (f:t–1-1→B → f:t–→B)
13		ffvelrn 3820	. . . . . . . . . . . 12 ⊢ ((f:t–→B ⋀ ∪ran { x} ∈ t) → (f ‘∪ran { x}) ∈ B)
14	13	ex 373	. . . . . . . . . . 11 ⊢ (f:t–→B → (∪ran { x} ∈ t → (f ‘∪ran { x}) ∈ B))
15	12, 14	syl 10	. . . . . . . . . 10 ⊢ (f:t–1-1→B → (∪ran { x} ∈ t → (f ‘∪ran { x}) ∈ B))
16	15	anim2d 563	. . . . . . . . 9 ⊢ (f:t–1-1→B → ((∪dom { x} ∈ C ⋀ ∪ran { x} ∈ t) → (∪dom { x} ∈ C ⋀ (f ‘∪ran { x}) ∈ B)))
17	16	adantld 392	. . . . . . . 8 ⊢ (f:t–1-1→B → ((x = ⟨∪dom { x}, ∪ran { x}⟩ ⋀ (∪dom { x} ∈ C ⋀ ∪ran { x} ∈ t)) → (∪dom { x} ∈ C ⋀ (f ‘∪ran { x}) ∈ B)))
18		elxp4 3459	. . . . . . . 8 ⊢ (x ∈ (C × t) ↔ (x = ⟨∪dom { x}, ∪ran { x}⟩ ⋀ (∪dom { x} ∈ C ⋀ ∪ran { x} ∈ t)))
19		fvex 3738	. . . . . . . . 9 ⊢ (f ‘∪ran { x}) ∈ V
20	19	opelxp 3220	. . . . . . . 8 ⊢ (⟨∪dom { x}, (f ‘∪ran { x})⟩ ∈ (C × B) ↔ (∪dom { x} ∈ C ⋀ (f ‘∪ran { x}) ∈ B))
21	17, 18, 20	3imtr4g 555	. . . . . . 7 ⊢ (f:t–1-1→B → (x ∈ (C × t) → ⟨∪dom { x}, (f ‘∪ran { x})⟩ ∈ (C × B)))
22		f1fveq 3882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((f:t–1-1→B ⋀ (w ∈ t ⋀ u ∈ t)) → ((f ‘w) = (f ‘u) ↔ w = u))
23	22	ancoms 438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((w ∈ t ⋀ u ∈ t) ⋀ f:t–1-1→B) → ((f ‘w) = (f ‘u) ↔ w = u))
24	23	anbi2d 618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((w ∈ t ⋀ u ∈ t) ⋀ f:t–1-1→B) → ((z = v ⋀ (f ‘w) = (f ‘u)) ↔ (z = v ⋀ w = u)))
25		visset 1816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ z ∈ V
26		fvex 3738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f ‘w) ∈ V
27		fvex 3738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (f ‘u) ∈ V
28	25, 26, 27	opth 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ⋀ (f ‘w) = (f ‘u)))
29	24, 28	syl5bb 534	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((w ∈ t ⋀ u ∈ t) ⋀ f:t–1-1→B) → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ⋀ w = u)))
30	29	ex 373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((w ∈ t ⋀ u ∈ t) → (f:t–1-1→B → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ⋀ w = u))))
31	30	ad2ant2l 410	. . . . . . . . . . . . . . . . . 18 ⊢ (((z ∈ C ⋀ w ∈ t) ⋀ (v ∈ C ⋀ u ∈ t)) → (f:t–1-1→B → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ⋀ w = u))))
32	31	imp 350	. . . . . . . . . . . . . . . . 17 ⊢ ((((z ∈ C ⋀ w ∈ t) ⋀ (v ∈ C ⋀ u ∈ t)) ⋀ f:t–1-1→B) → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ⋀ w = u)))
33	32	adantlr 395	. . . . . . . . . . . . . . . 16 ⊢ (((((z ∈ C ⋀ w ∈ t) ⋀ (v ∈ C ⋀ u ∈ t)) ⋀ (x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩)) ⋀ f:t–1-1→B) → (⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩ ↔ (z = v ⋀ w = u)))
34		sneq 2421	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = ⟨z, w⟩ → {x} = {⟨z, w⟩})
35	34	dmeqd 3319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = ⟨z, w⟩ → dom { x} = dom {⟨z, w⟩})
36	35	unieqd 2516	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = ⟨z, w⟩ → ∪dom { x} = ∪dom {⟨z, w⟩})
37	25	op1sta 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪dom {⟨z, w⟩} = z
38	36, 37	syl6eq 1526	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = ⟨z, w⟩ → ∪dom { x} = z)
39	34	rneqd 3347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = ⟨z, w⟩ → ran { x} = ran {⟨z, w⟩})
40	39	unieqd 2516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = ⟨z, w⟩ → ∪ran { x} = ∪ran {⟨z, w⟩})
41		visset 1816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ w ∈ V
42	25, 41	op2nda 3458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ran {⟨z, w⟩} = w
43	40, 42	syl6eq 1526	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = ⟨z, w⟩ → ∪ran { x} = w)
44	43	fveq2d 3734	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = ⟨z, w⟩ → (f ‘∪ran { x}) = (f ‘w))
45	38, 44	opeq12d 2499	. . . . . . . . . . . . . . . . . 18 ⊢ (x = ⟨z, w⟩ → ⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨z, (f ‘w)⟩)
46		sneq 2421	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = ⟨v, u⟩ → {y} = {⟨v, u⟩})
47	46	dmeqd 3319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = ⟨v, u⟩ → dom { y} = dom {⟨v, u⟩})
48	47	unieqd 2516	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = ⟨v, u⟩ → ∪dom { y} = ∪dom {⟨v, u⟩})
49		visset 1816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ v ∈ V
50	49	op1sta 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪dom {⟨v, u⟩} = v
51	48, 50	syl6eq 1526	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = ⟨v, u⟩ → ∪dom { y} = v)
52	46	rneqd 3347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = ⟨v, u⟩ → ran { y} = ran {⟨v, u⟩})
53	52	unieqd 2516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = ⟨v, u⟩ → ∪ran { y} = ∪ran {⟨v, u⟩})
54		visset 1816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ u ∈ V
55	49, 54	op2nda 3458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ran {⟨v, u⟩} = u
56	53, 55	syl6eq 1526	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = ⟨v, u⟩ → ∪ran { y} = u)
57	56	fveq2d 3734	. . . . . . . . . . . . . . . . . . 19 ⊢ (y = ⟨v, u⟩ → (f ‘∪ran { y}) = (f ‘u))
58	51, 57	opeq12d 2499	. . . . . . . . . . . . . . . . . 18 ⊢ (y = ⟨v, u⟩ → ⟨∪dom { y}, (f ‘∪ran { y})⟩ = ⟨v, (f ‘u)⟩)
59	45, 58	eqeqan12d 1493	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩) → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ ⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩))
60	59	ad2antlr 407	. . . . . . . . . . . . . . . 16 ⊢ (((((z ∈ C ⋀ w ∈ t) ⋀ (v ∈ C ⋀ u ∈ t)) ⋀ (x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩)) ⋀ f:t–1-1→B) → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ ⟨z, (f ‘w)⟩ = ⟨v, (f ‘u)⟩))
61		eqeq12 1490	. . . . . . . . . . . . . . . . . 18 ⊢ ((x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩) → (x = y ↔ ⟨z, w⟩ = ⟨v, u⟩))
62	25, 41, 54	opth 2793	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨z, w⟩ = ⟨v, u⟩ ↔ (z = v ⋀ w = u))
63	61, 62	syl6bb 538	. . . . . . . . . . . . . . . . 17 ⊢ ((x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩) → (x = y ↔ (z = v ⋀ w = u)))
64	63	ad2antlr 407	. . . . . . . . . . . . . . . 16 ⊢ (((((z ∈ C ⋀ w ∈ t) ⋀ (v ∈ C ⋀ u ∈ t)) ⋀ (x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩)) ⋀ f:t–1-1→B) → (x = y ↔ (z = v ⋀ w = u)))
65	33, 60, 64	3bitr4d 552	. . . . . . . . . . . . . . 15 ⊢ (((((z ∈ C ⋀ w ∈ t) ⋀ (v ∈ C ⋀ u ∈ t)) ⋀ (x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩)) ⋀ f:t–1-1→B) → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y))
66	65	ex 373	. . . . . . . . . . . . . 14 ⊢ ((((z ∈ C ⋀ w ∈ t) ⋀ (v ∈ C ⋀ u ∈ t)) ⋀ (x = ⟨z, w⟩ ⋀ y = ⟨v, u⟩)) → (f:t–1-1→B → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y)))
67	66	exp43 386	. . . . . . . . . . . . 13 ⊢ ((z ∈ C ⋀ w ∈ t) → ((v ∈ C ⋀ u ∈ t) → (x = ⟨z, w⟩ → (y = ⟨v, u⟩ → (f:t–1-1→B → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y))))))
68	67	com23 32	. . . . . . . . . . . 12 ⊢ ((z ∈ C ⋀ w ∈ t) → (x = ⟨z, w⟩ → ((v ∈ C ⋀ u ∈ t) → (y = ⟨v, u⟩ → (f:t–1-1→B → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y))))))
69	68	r19.23aivv 1751	. . . . . . . . . . 11 ⊢ (∃z ∈ C ∃w ∈ t x = ⟨z, w⟩ → ((v ∈ C ⋀ u ∈ t) → (y = ⟨v, u⟩ → (f:t–1-1→B → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y)))))
70	69	r19.23advv 1752	. . . . . . . . . 10 ⊢ (∃z ∈ C ∃w ∈ t x = ⟨z, w⟩ → (∃v ∈ C ∃u ∈ t y = ⟨v, u⟩ → (f:t–1-1→B → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y))))
71	70	imp 350	. . . . . . . . 9 ⊢ ((∃z ∈ C ∃w ∈ t x = ⟨z, w⟩ ⋀ ∃v ∈ C ∃u ∈ t y = ⟨v, u⟩) → (f:t–1-1→B → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y)))
72		elxp2 3209	. . . . . . . . 9 ⊢ (x ∈ (C × t) ↔ ∃z ∈ C ∃w ∈ t x = ⟨z, w⟩)
73		elxp2 3209	. . . . . . . . 9 ⊢ (y ∈ (C × t) ↔ ∃v ∈ C ∃u ∈ t y = ⟨v, u⟩)
74	71, 72, 73	syl2anb 457	. . . . . . . 8 ⊢ ((x ∈ (C × t) ⋀ y ∈ (C × t)) → (f:t–1-1→B → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y)))
75	74	com12 11	. . . . . . 7 ⊢ (f:t–1-1→B → ((x ∈ (C × t) ⋀ y ∈ (C × t)) → (⟨∪dom { x}, (f ‘∪ran { x})⟩ = ⟨∪dom { y}, (f ‘∪ran { y})⟩ ↔ x = y)))
76	21, 75	dom2d 4410	. . . . . 6 ⊢ (f:t–1-1→B → ((C × t) ∈ V → (C × t) ≼ (C × B)))
77	11, 76	mpi 44	. . . . 5 ⊢ (f:t–1-1→B → (C × t) ≼ (C × B))
78	77	19.23aiv 1297	. . . 4 ⊢ (∃f f:t–1-1→B → (C × t) ≼ (C × B))
79	8, 78	sylbi 199	. . 3 ⊢ (t ≼ B → (C × t) ≼ (C × B))
80	6, 79	vtoclg 1850	. 2 ⊢ (A ∈ V → (A ≼ B → (C × A) ≼ (C × B)))
81	2, 80	mpcom 49	1 ⊢ (A ≼ B → (C × A) ≼ (C × B))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 958   ∈ wcel 960  ∃wex 982  ∃wrex 1649  Vcvv 1814  {csn 2413  ⟨cop 2415  ∪cuni 2507   class class class wbr 2624   × cxp 3174  dom cdm 3176  ran crn 3177  –→wf 3184  –1-1→wf1 3185   ‘cfv 3188   ≼ cdom 4371

This theorem is referenced by:  xpdom1 4449  xpen 4494  infunabs 7566  infcdaabs 7567  infxpabs 7571

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-id 2841  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203  df-fv 3204  df-en 4374  df-dom 4375

Copyright terms: Public domain