xpdom2

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)

		Ref	Expression
	Hypothesis	xpdom.2	$⊢ C \in V$
	Assertion	xpdom2	$⊢ A ≼ B \to (C \times A) ≼ (C \times B)$

Proof

Step	Hyp	Ref	Expression
1		xpdom.2	$⊢ C \in V$
2		brdomi	$⊢ A ≼ B \to \exists f f : A \underset{1-1}{⟶} B$
3		f1f	$⊢ f : A \underset{1-1}{⟶} B \to f : A ⟶ B$
4		ffvelcdm	$⊢ (f : A ⟶ B \land ⋃ ran \{x\} \in A) \to f (⋃ ran \{x\}) \in B$
5	4	ex	$⊢ f : A ⟶ B \to (⋃ ran \{x\} \in A \to f (⋃ ran \{x\}) \in B)$
6	3 5	syl	$⊢ f : A \underset{1-1}{⟶} B \to (⋃ ran \{x\} \in A \to f (⋃ ran \{x\}) \in B)$
7	6	anim2d	$⊢ f : A \underset{1-1}{⟶} B \to ((⋃ dom \{x\} \in C \land ⋃ ran \{x\} \in A) \to (⋃ dom \{x\} \in C \land f (⋃ ran \{x\}) \in B))$
8	7	adantld	$⊢ f : A \underset{1-1}{⟶} B \to ((x = ⟨⋃ dom \{x\}, ⋃ ran \{x\}⟩ \land (⋃ dom \{x\} \in C \land ⋃ ran \{x\} \in A)) \to (⋃ dom \{x\} \in C \land f (⋃ ran \{x\}) \in B))$
9		elxp4	$⊢ x \in (C \times A) \leftrightarrow (x = ⟨⋃ dom \{x\}, ⋃ ran \{x\}⟩ \land (⋃ dom \{x\} \in C \land ⋃ ran \{x\} \in A))$
10		opelxp	$⊢ ⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ \in (C \times B) \leftrightarrow (⋃ dom \{x\} \in C \land f (⋃ ran \{x\}) \in B)$
11	8 9 10	3imtr4g	$⊢ f : A \underset{1-1}{⟶} B \to (x \in (C \times A) \to ⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ \in (C \times B))$
12	11	adantl	$⊢ (A ≼ B \land f : A \underset{1-1}{⟶} B) \to (x \in (C \times A) \to ⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ \in (C \times B))$
13		elxp2	$⊢ x \in (C \times A) \leftrightarrow \exists z \in C \exists w \in A x = ⟨z, w⟩$
14		elxp2	$⊢ y \in (C \times A) \leftrightarrow \exists v \in C \exists u \in A y = ⟨v, u⟩$
15		vex	$⊢ z \in V$
16		fvex	$⊢ f (w) \in V$
17	15 16	opth	$⊢ ⟨z, f (w)⟩ = ⟨v, f (u)⟩ \leftrightarrow (z = v \land f (w) = f (u))$
18		f1fveq	$⊢ (f : A \underset{1-1}{⟶} B \land (w \in A \land u \in A)) \to (f (w) = f (u) \leftrightarrow w = u)$
19	18	ancoms	$⊢ ((w \in A \land u \in A) \land f : A \underset{1-1}{⟶} B) \to (f (w) = f (u) \leftrightarrow w = u)$
20	19	anbi2d	$⊢ ((w \in A \land u \in A) \land f : A \underset{1-1}{⟶} B) \to ((z = v \land f (w) = f (u)) \leftrightarrow (z = v \land w = u))$
21	17 20	bitrid	$⊢ ((w \in A \land u \in A) \land f : A \underset{1-1}{⟶} B) \to (⟨z, f (w)⟩ = ⟨v, f (u)⟩ \leftrightarrow (z = v \land w = u))$
22	21	ex	$⊢ (w \in A \land u \in A) \to (f : A \underset{1-1}{⟶} B \to (⟨z, f (w)⟩ = ⟨v, f (u)⟩ \leftrightarrow (z = v \land w = u)))$
23	22	ad2ant2l	$⊢ ((z \in C \land w \in A) \land (v \in C \land u \in A)) \to (f : A \underset{1-1}{⟶} B \to (⟨z, f (w)⟩ = ⟨v, f (u)⟩ \leftrightarrow (z = v \land w = u)))$
24	23	imp	$⊢ (((z \in C \land w \in A) \land (v \in C \land u \in A)) \land f : A \underset{1-1}{⟶} B) \to (⟨z, f (w)⟩ = ⟨v, f (u)⟩ \leftrightarrow (z = v \land w = u))$
25	24	adantlr	$⊢ ((((z \in C \land w \in A) \land (v \in C \land u \in A)) \land (x = ⟨z, w⟩ \land y = ⟨v, u⟩)) \land f : A \underset{1-1}{⟶} B) \to (⟨z, f (w)⟩ = ⟨v, f (u)⟩ \leftrightarrow (z = v \land w = u))$
26		sneq	$⊢ x = ⟨z, w⟩ \to \{x\} = \{⟨z, w⟩\}$
27	26	dmeqd	$⊢ x = ⟨z, w⟩ \to dom \{x\} = dom \{⟨z, w⟩\}$
28	27	unieqd	$⊢ x = ⟨z, w⟩ \to ⋃ dom \{x\} = ⋃ dom \{⟨z, w⟩\}$
29		vex	$⊢ w \in V$
30	15 29	op1sta	$⊢ ⋃ dom \{⟨z, w⟩\} = z$
31	28 30	eqtrdi	$⊢ x = ⟨z, w⟩ \to ⋃ dom \{x\} = z$
32	26	rneqd	$⊢ x = ⟨z, w⟩ \to ran \{x\} = ran \{⟨z, w⟩\}$
33	32	unieqd	$⊢ x = ⟨z, w⟩ \to ⋃ ran \{x\} = ⋃ ran \{⟨z, w⟩\}$
34	15 29	op2nda	$⊢ ⋃ ran \{⟨z, w⟩\} = w$
35	33 34	eqtrdi	$⊢ x = ⟨z, w⟩ \to ⋃ ran \{x\} = w$
36	35	fveq2d	$⊢ x = ⟨z, w⟩ \to f (⋃ ran \{x\}) = f (w)$
37	31 36	opeq12d	$⊢ x = ⟨z, w⟩ \to ⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨z, f (w)⟩$
38		sneq	$⊢ y = ⟨v, u⟩ \to \{y\} = \{⟨v, u⟩\}$
39	38	dmeqd	$⊢ y = ⟨v, u⟩ \to dom \{y\} = dom \{⟨v, u⟩\}$
40	39	unieqd	$⊢ y = ⟨v, u⟩ \to ⋃ dom \{y\} = ⋃ dom \{⟨v, u⟩\}$
41		vex	$⊢ v \in V$
42		vex	$⊢ u \in V$
43	41 42	op1sta	$⊢ ⋃ dom \{⟨v, u⟩\} = v$
44	40 43	eqtrdi	$⊢ y = ⟨v, u⟩ \to ⋃ dom \{y\} = v$
45	38	rneqd	$⊢ y = ⟨v, u⟩ \to ran \{y\} = ran \{⟨v, u⟩\}$
46	45	unieqd	$⊢ y = ⟨v, u⟩ \to ⋃ ran \{y\} = ⋃ ran \{⟨v, u⟩\}$
47	41 42	op2nda	$⊢ ⋃ ran \{⟨v, u⟩\} = u$
48	46 47	eqtrdi	$⊢ y = ⟨v, u⟩ \to ⋃ ran \{y\} = u$
49	48	fveq2d	$⊢ y = ⟨v, u⟩ \to f (⋃ ran \{y\}) = f (u)$
50	44 49	opeq12d	$⊢ y = ⟨v, u⟩ \to ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ = ⟨v, f (u)⟩$
51	37 50	eqeqan12d	$⊢ (x = ⟨z, w⟩ \land y = ⟨v, u⟩) \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow ⟨z, f (w)⟩ = ⟨v, f (u)⟩)$
52	51	ad2antlr	$⊢ ((((z \in C \land w \in A) \land (v \in C \land u \in A)) \land (x = ⟨z, w⟩ \land y = ⟨v, u⟩)) \land f : A \underset{1-1}{⟶} B) \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow ⟨z, f (w)⟩ = ⟨v, f (u)⟩)$
53		eqeq12	$⊢ (x = ⟨z, w⟩ \land y = ⟨v, u⟩) \to (x = y \leftrightarrow ⟨z, w⟩ = ⟨v, u⟩)$
54	15 29	opth	$⊢ ⟨z, w⟩ = ⟨v, u⟩ \leftrightarrow (z = v \land w = u)$
55	53 54	bitrdi	$⊢ (x = ⟨z, w⟩ \land y = ⟨v, u⟩) \to (x = y \leftrightarrow (z = v \land w = u))$
56	55	ad2antlr	$⊢ ((((z \in C \land w \in A) \land (v \in C \land u \in A)) \land (x = ⟨z, w⟩ \land y = ⟨v, u⟩)) \land f : A \underset{1-1}{⟶} B) \to (x = y \leftrightarrow (z = v \land w = u))$
57	25 52 56	3bitr4d	$⊢ ((((z \in C \land w \in A) \land (v \in C \land u \in A)) \land (x = ⟨z, w⟩ \land y = ⟨v, u⟩)) \land f : A \underset{1-1}{⟶} B) \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y)$
58	57	exp53	$⊢ (z \in C \land w \in A) \to ((v \in C \land u \in A) \to (x = ⟨z, w⟩ \to (y = ⟨v, u⟩ \to (f : A \underset{1-1}{⟶} B \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y)))))$
59	58	com23	$⊢ (z \in C \land w \in A) \to (x = ⟨z, w⟩ \to ((v \in C \land u \in A) \to (y = ⟨v, u⟩ \to (f : A \underset{1-1}{⟶} B \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y)))))$
60	59	rexlimivv	$⊢ \exists z \in C \exists w \in A x = ⟨z, w⟩ \to ((v \in C \land u \in A) \to (y = ⟨v, u⟩ \to (f : A \underset{1-1}{⟶} B \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y))))$
61	60	rexlimdvv	$⊢ \exists z \in C \exists w \in A x = ⟨z, w⟩ \to (\exists v \in C \exists u \in A y = ⟨v, u⟩ \to (f : A \underset{1-1}{⟶} B \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y)))$
62	61	imp	$⊢ (\exists z \in C \exists w \in A x = ⟨z, w⟩ \land \exists v \in C \exists u \in A y = ⟨v, u⟩) \to (f : A \underset{1-1}{⟶} B \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y))$
63	13 14 62	syl2anb	$⊢ (x \in (C \times A) \land y \in (C \times A)) \to (f : A \underset{1-1}{⟶} B \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y))$
64	63	com12	$⊢ f : A \underset{1-1}{⟶} B \to ((x \in (C \times A) \land y \in (C \times A)) \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y))$
65	64	adantl	$⊢ (A ≼ B \land f : A \underset{1-1}{⟶} B) \to ((x \in (C \times A) \land y \in (C \times A)) \to (⟨⋃ dom \{x\}, f (⋃ ran \{x\})⟩ = ⟨⋃ dom \{y\}, f (⋃ ran \{y\})⟩ \leftrightarrow x = y))$
66		reldom	$⊢ Rel ≼$
67	66	brrelex1i	$⊢ A ≼ B \to A \in V$
68		xpexg	$⊢ (C \in V \land A \in V) \to C \times A \in V$
69	1 67 68	sylancr	$⊢ A ≼ B \to C \times A \in V$
70	69	adantr	$⊢ (A ≼ B \land f : A \underset{1-1}{⟶} B) \to C \times A \in V$
71	66	brrelex2i	$⊢ A ≼ B \to B \in V$
72		xpexg	$⊢ (C \in V \land B \in V) \to C \times B \in V$
73	1 71 72	sylancr	$⊢ A ≼ B \to C \times B \in V$
74	73	adantr	$⊢ (A ≼ B \land f : A \underset{1-1}{⟶} B) \to C \times B \in V$
75	12 65 70 74	dom3d	$⊢ (A ≼ B \land f : A \underset{1-1}{⟶} B) \to (C \times A) ≼ (C \times B)$
76	2 75	exlimddv	$⊢ A ≼ B \to (C \times A) ≼ (C \times B)$

Metamath Proof Explorer

Theorem xpdom2

Proof