unxpdomlem3

	Ref	Expression
Hypotheses	unxpdomlem1.1	$⊢ F = (x \in (a \cup b) ⟼ G)$
	unxpdomlem1.2	$⊢ G = if (x \in a, ⟨x, if (x = m, t, s)⟩, ⟨if (x = t, n, m), x⟩)$
Assertion	unxpdomlem3	$⊢ (1_{𝑜} ≺ a \land 1_{𝑜} ≺ b) \to (a \cup b) ≼ (a \times b)$

Proof

Step	Hyp	Ref	Expression
1		unxpdomlem1.1	$⊢ F = (x \in (a \cup b) ⟼ G)$
2		unxpdomlem1.2	$⊢ G = if (x \in a, ⟨x, if (x = m, t, s)⟩, ⟨if (x = t, n, m), x⟩)$
3		1sdom	$⊢ a \in V \to (1_{𝑜} ≺ a \leftrightarrow \exists m \in a \exists n \in a \neg m = n)$
4	3	elv	$⊢ 1_{𝑜} ≺ a \leftrightarrow \exists m \in a \exists n \in a \neg m = n$
5		1sdom	$⊢ b \in V \to (1_{𝑜} ≺ b \leftrightarrow \exists s \in b \exists t \in b \neg s = t)$
6	5	elv	$⊢ 1_{𝑜} ≺ b \leftrightarrow \exists s \in b \exists t \in b \neg s = t$
7		reeanv	$⊢ \exists m \in a \exists s \in b (\exists n \in a \neg m = n \land \exists t \in b \neg s = t) \leftrightarrow (\exists m \in a \exists n \in a \neg m = n \land \exists s \in b \exists t \in b \neg s = t)$
8		reeanv	$⊢ \exists n \in a \exists t \in b (\neg m = n \land \neg s = t) \leftrightarrow (\exists n \in a \neg m = n \land \exists t \in b \neg s = t)$
9		vex	$⊢ a \in V$
10		vex	$⊢ b \in V$
11	9 10	unex	$⊢ a \cup b \in V$
12	9 10	xpex	$⊢ a \times b \in V$
13		simpr	$⊢ ((((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \land x \in a) \to x \in a$
14		simp2r	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to t \in b$
15		simp1r	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to s \in b$
16	14 15	ifcld	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to if (x = m, t, s) \in b$
17	16	ad2antrr	$⊢ ((((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \land x \in a) \to if (x = m, t, s) \in b$
18	13 17	opelxpd	$⊢ ((((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \land x \in a) \to ⟨x, if (x = m, t, s)⟩ \in (a \times b)$
19		simp2l	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to n \in a$
20		simp1l	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to m \in a$
21	19 20	ifcld	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to if (x = t, n, m) \in a$
22	21	ad2antrr	$⊢ ((((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \land \neg x \in a) \to if (x = t, n, m) \in a$
23		elun	$⊢ x \in (a \cup b) \leftrightarrow (x \in a \lor x \in b)$
24	23	bilani	$⊢ (((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \to (x \in a \lor x \in b)$
25	24	orcanai	$⊢ ((((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \land \neg x \in a) \to x \in b$
26	22 25	opelxpd	$⊢ ((((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \land \neg x \in a) \to ⟨if (x = t, n, m), x⟩ \in (a \times b)$
27	18 26	ifclda	$⊢ (((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \to if (x \in a, ⟨x, if (x = m, t, s)⟩, ⟨if (x = t, n, m), x⟩) \in (a \times b)$
28	2 27	eqeltrid	$⊢ (((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \land x \in (a \cup b)) \to G \in (a \times b)$
29	28 1	fmptd	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to F : a \cup b ⟶ a \times b$
30	1 2	unxpdomlem1	$⊢ z \in (a \cup b) \to F (z) = if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩)$
31	30	ad2antrl	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to F (z) = if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩)$
32		iftrue	$⊢ z \in a \to if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩) = ⟨z, if (z = m, t, s)⟩$
33	32	adantr	$⊢ (z \in a \land w \in a) \to if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩) = ⟨z, if (z = m, t, s)⟩$
34	31 33	sylan9eq	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (z \in a \land w \in a)) \to F (z) = ⟨z, if (z = m, t, s)⟩$
35	1 2	unxpdomlem1	$⊢ w \in (a \cup b) \to F (w) = if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩)$
36	35	ad2antll	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to F (w) = if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩)$
37		iftrue	$⊢ w \in a \to if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩) = ⟨w, if (w = m, t, s)⟩$
38	37	adantl	$⊢ (z \in a \land w \in a) \to if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩) = ⟨w, if (w = m, t, s)⟩$
39	36 38	sylan9eq	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (z \in a \land w \in a)) \to F (w) = ⟨w, if (w = m, t, s)⟩$
40	34 39	eqeq12d	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (z \in a \land w \in a)) \to (F (z) = F (w) \leftrightarrow ⟨z, if (z = m, t, s)⟩ = ⟨w, if (w = m, t, s)⟩)$
41		vex	$⊢ z \in V$
42		vex	$⊢ t \in V$
43		vex	$⊢ s \in V$
44	42 43	ifex	$⊢ if (z = m, t, s) \in V$
45	41 44	opth1	$⊢ ⟨z, if (z = m, t, s)⟩ = ⟨w, if (w = m, t, s)⟩ \to z = w$
46	40 45	biimtrdi	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (z \in a \land w \in a)) \to (F (z) = F (w) \to z = w)$
47		simprr	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to w \in (a \cup b)$
48		simpll	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to \neg m = n$
49		simplr	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to \neg s = t$
50	1 2 47 48 49	unxpdomlem2	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (z \in a \land \neg w \in a)) \to \neg F (z) = F (w)$
51	50	pm2.21d	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (z \in a \land \neg w \in a)) \to (F (z) = F (w) \to z = w)$
52		eqcom	$⊢ F (z) = F (w) \leftrightarrow F (w) = F (z)$
53		simprl	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to z \in (a \cup b)$
54	1 2 53 48 49	unxpdomlem2	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (w \in a \land \neg z \in a)) \to \neg F (w) = F (z)$
55	54	ancom2s	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (\neg z \in a \land w \in a)) \to \neg F (w) = F (z)$
56	55	pm2.21d	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (\neg z \in a \land w \in a)) \to (F (w) = F (z) \to z = w)$
57	52 56	biimtrid	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (\neg z \in a \land w \in a)) \to (F (z) = F (w) \to z = w)$
58		iffalse	$⊢ \neg z \in a \to if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩) = ⟨if (z = t, n, m), z⟩$
59	58	adantr	$⊢ (\neg z \in a \land \neg w \in a) \to if (z \in a, ⟨z, if (z = m, t, s)⟩, ⟨if (z = t, n, m), z⟩) = ⟨if (z = t, n, m), z⟩$
60	31 59	sylan9eq	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (\neg z \in a \land \neg w \in a)) \to F (z) = ⟨if (z = t, n, m), z⟩$
61		iffalse	$⊢ \neg w \in a \to if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩) = ⟨if (w = t, n, m), w⟩$
62	61	adantl	$⊢ (\neg z \in a \land \neg w \in a) \to if (w \in a, ⟨w, if (w = m, t, s)⟩, ⟨if (w = t, n, m), w⟩) = ⟨if (w = t, n, m), w⟩$
63	36 62	sylan9eq	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (\neg z \in a \land \neg w \in a)) \to F (w) = ⟨if (w = t, n, m), w⟩$
64	60 63	eqeq12d	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (\neg z \in a \land \neg w \in a)) \to (F (z) = F (w) \leftrightarrow ⟨if (z = t, n, m), z⟩ = ⟨if (w = t, n, m), w⟩)$
65		vex	$⊢ n \in V$
66		vex	$⊢ m \in V$
67	65 66	ifex	$⊢ if (z = t, n, m) \in V$
68	67 41	opth	$⊢ ⟨if (z = t, n, m), z⟩ = ⟨if (w = t, n, m), w⟩ \leftrightarrow (if (z = t, n, m) = if (w = t, n, m) \land z = w)$
69	68	simprbi	$⊢ ⟨if (z = t, n, m), z⟩ = ⟨if (w = t, n, m), w⟩ \to z = w$
70	64 69	biimtrdi	$⊢ (((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \land (\neg z \in a \land \neg w \in a)) \to (F (z) = F (w) \to z = w)$
71	46 51 57 70	4casesdan	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to (F (z) = F (w) \to z = w)$
72	71	ralrimivva	$⊢ (\neg m = n \land \neg s = t) \to \forall z \in (a \cup b) \forall w \in (a \cup b) (F (z) = F (w) \to z = w)$
73	72	3ad2ant3	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to \forall z \in (a \cup b) \forall w \in (a \cup b) (F (z) = F (w) \to z = w)$
74		dff13	$⊢ F : a \cup b \underset{1-1}{⟶} a \times b \leftrightarrow (F : a \cup b ⟶ a \times b \land \forall z \in (a \cup b) \forall w \in (a \cup b) (F (z) = F (w) \to z = w))$
75	29 73 74	sylanbrc	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to F : a \cup b \underset{1-1}{⟶} a \times b$
76		f1dom2g	$⊢ (a \cup b \in V \land a \times b \in V \land F : a \cup b \underset{1-1}{⟶} a \times b) \to (a \cup b) ≼ (a \times b)$
77	11 12 75 76	mp3an12i	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b) \land (\neg m = n \land \neg s = t)) \to (a \cup b) ≼ (a \times b)$
78	77	3expia	$⊢ ((m \in a \land s \in b) \land (n \in a \land t \in b)) \to ((\neg m = n \land \neg s = t) \to (a \cup b) ≼ (a \times b))$
79	78	rexlimdvva	$⊢ (m \in a \land s \in b) \to (\exists n \in a \exists t \in b (\neg m = n \land \neg s = t) \to (a \cup b) ≼ (a \times b))$
80	8 79	biimtrrid	$⊢ (m \in a \land s \in b) \to ((\exists n \in a \neg m = n \land \exists t \in b \neg s = t) \to (a \cup b) ≼ (a \times b))$
81	80	rexlimivv	$⊢ \exists m \in a \exists s \in b (\exists n \in a \neg m = n \land \exists t \in b \neg s = t) \to (a \cup b) ≼ (a \times b)$
82	7 81	sylbir	$⊢ (\exists m \in a \exists n \in a \neg m = n \land \exists s \in b \exists t \in b \neg s = t) \to (a \cup b) ≼ (a \times b)$
83	4 6 82	syl2anb	$⊢ (1_{𝑜} ≺ a \land 1_{𝑜} ≺ b) \to (a \cup b) ≼ (a \times b)$

Metamath Proof Explorer

Theorem unxpdomlem3

Proof