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		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)) \to x \in (a \cup b)$
24		elun	$⊢ x \in (a \cup b) \leftrightarrow (x \in a \lor x \in b)$
25	23 24	sylib	$⊢ (((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)$
26	25	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$
27	22 26	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)$
28	18 27	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)$
29	2 28	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)$
30	29 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$
31	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⟩)$
32	31	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⟩)$
33		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)⟩$
34	33	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)⟩$
35	32 34	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)⟩$
36	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⟩)$
37	36	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⟩)$
38		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)⟩$
39	38	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)⟩$
40	37 39	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)⟩$
41	35 40	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)⟩)$
42		vex	$⊢ z \in V$
43		vex	$⊢ t \in V$
44		vex	$⊢ s \in V$
45	43 44	ifex	$⊢ if (z = m, t, s) \in V$
46	42 45	opth1	$⊢ ⟨z, if (z = m, t, s)⟩ = ⟨w, if (w = m, t, s)⟩ \to z = w$
47	41 46	syl6bi	$⊢ (((\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)$
48		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)$
49		simpll	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to \neg m = n$
50		simplr	$⊢ ((\neg m = n \land \neg s = t) \land (z \in (a \cup b) \land w \in (a \cup b))) \to \neg s = t$
51	1 2 48 49 50	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)$
52	51	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)$
53		eqcom	$⊢ F (z) = F (w) \leftrightarrow F (w) = F (z)$
54		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)$
55	1 2 54 49 50	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)$
56	55	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)$
57	56	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)$
58	53 57	syl5bi	$⊢ (((\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)$
59		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⟩$
60	59	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⟩$
61	32 60	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⟩$
62		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⟩$
63	62	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⟩$
64	37 63	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⟩$
65	61 64	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⟩)$
66		vex	$⊢ n \in V$
67		vex	$⊢ m \in V$
68	66 67	ifex	$⊢ if (z = t, n, m) \in V$
69	68 42	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)$
70	69	simprbi	$⊢ ⟨if (z = t, n, m), z⟩ = ⟨if (w = t, n, m), w⟩ \to z = w$
71	65 70	syl6bi	$⊢ (((\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)$
72	47 52 58 71	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)$
73	72	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)$
74	73	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)$
75		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))$
76	30 74 75	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$
77		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)$
78	11 12 76 77	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)$
79	78	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))$
80	79	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))$
81	8 80	syl5bir	$⊢ (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))$
82	81	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)$
83	7 82	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)$
84	4 6 83	syl2anb	$⊢ (1_{𝑜} ≺ a \land 1_{𝑜} ≺ b) \to (a \cup b) ≼ (a \times b)$

Metamath Proof Explorer

Theorem unxpdomlem3

Proof