scutun12

Description: Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021)

		Ref	Expression
	Assertion	scutun12	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (A \cup C) \|_{s} (B \cup D) = A \|_{s} B$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to A ≪_{s} B$
2		scutcut	$⊢ A ≪_{s} B \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
3	1 2	syl	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
4	3	simp2d	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to A ≪_{s} \{A \|_{s} B\}$
5		simp2	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to C ≪_{s} \{A \|_{s} B\}$
6		ssltun1	$⊢ (A ≪_{s} \{A \|_{s} B\} \land C ≪_{s} \{A \|_{s} B\}) \to (A \cup C) ≪_{s} \{A \|_{s} B\}$
7	4 5 6	syl2anc	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (A \cup C) ≪_{s} \{A \|_{s} B\}$
8	3	simp3d	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to \{A \|_{s} B\} ≪_{s} B$
9		simp3	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to \{A \|_{s} B\} ≪_{s} D$
10		ssltun2	$⊢ (\{A \|_{s} B\} ≪_{s} B \land \{A \|_{s} B\} ≪_{s} D) \to \{A \|_{s} B\} ≪_{s} (B \cup D)$
11	8 9 10	syl2anc	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to \{A \|_{s} B\} ≪_{s} (B \cup D)$
12		ovex	$⊢ A \|_{s} B \in V$
13	12	snnz	$⊢ \{A \|_{s} B\} \neq \emptyset$
14		sslttr	$⊢ ((A \cup C) ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} (B \cup D) \land \{A \|_{s} B\} \neq \emptyset) \to (A \cup C) ≪_{s} (B \cup D)$
15	13 14	mp3an3	$⊢ ((A \cup C) ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} (B \cup D)) \to (A \cup C) ≪_{s} (B \cup D)$
16	7 11 15	syl2anc	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (A \cup C) ≪_{s} (B \cup D)$
17		scutval	$⊢ (A \cup C) ≪_{s} (B \cup D) \to (A \cup C) \|_{s} (B \cup D) = (ι x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \| bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}])$
18	16 17	syl	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (A \cup C) \|_{s} (B \cup D) = (ι x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \| bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}])$
19		vex	$⊢ x \in V$
20	19	elima	$⊢ x \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \leftrightarrow \exists z \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} z bday x$
21		sneq	$⊢ y = z \to \{y\} = \{z\}$
22	21	breq2d	$⊢ y = z \to ((A \cup C) ≪_{s} \{y\} \leftrightarrow (A \cup C) ≪_{s} \{z\})$
23	21	breq1d	$⊢ y = z \to (\{y\} ≪_{s} (B \cup D) \leftrightarrow \{z\} ≪_{s} (B \cup D))$
24	22 23	anbi12d	$⊢ y = z \to (((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D)) \leftrightarrow ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D)))$
25	24	rexrab	$⊢ \exists z \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} z bday x \leftrightarrow \exists z \in No (((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D)) \land z bday x)$
26	20 25	bitri	$⊢ x \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \leftrightarrow \exists z \in No (((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D)) \land z bday x)$
27		simplr	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to z \in No$
28		bdayfn	$⊢ bday Fn No$
29		fnbrfvb	$⊢ (bday Fn No \land z \in No) \to (bday (z) = x \leftrightarrow z bday x)$
30	28 29	mpan	$⊢ z \in No \to (bday (z) = x \leftrightarrow z bday x)$
31	27 30	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to (bday (z) = x \leftrightarrow z bday x)$
32		simpll1	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to A ≪_{s} B$
33		scutbday	$⊢ A ≪_{s} B \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
34	32 33	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
35		simprl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to (A \cup C) ≪_{s} \{z\}$
36		ssun1	$⊢ A \subseteq A \cup C$
37		sssslt1	$⊢ ((A \cup C) ≪_{s} \{z\} \land A \subseteq A \cup C) \to A ≪_{s} \{z\}$
38	36 37	mpan2	$⊢ (A \cup C) ≪_{s} \{z\} \to A ≪_{s} \{z\}$
39	35 38	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to A ≪_{s} \{z\}$
40		simprr	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to \{z\} ≪_{s} (B \cup D)$
41		ssun1	$⊢ B \subseteq B \cup D$
42		sssslt2	$⊢ (\{z\} ≪_{s} (B \cup D) \land B \subseteq B \cup D) \to \{z\} ≪_{s} B$
43	41 42	mpan2	$⊢ \{z\} ≪_{s} (B \cup D) \to \{z\} ≪_{s} B$
44	40 43	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to \{z\} ≪_{s} B$
45	39 44	jca	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to (A ≪_{s} \{z\} \land \{z\} ≪_{s} B)$
46	21	breq2d	$⊢ y = z \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{z\})$
47	21	breq1d	$⊢ y = z \to (\{y\} ≪_{s} B \leftrightarrow \{z\} ≪_{s} B)$
48	46 47	anbi12d	$⊢ y = z \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{z\} \land \{z\} ≪_{s} B))$
49	48	elrab	$⊢ z \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \leftrightarrow (z \in No \land (A ≪_{s} \{z\} \land \{z\} ≪_{s} B))$
50	27 45 49	sylanbrc	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to z \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}$
51		ssrab2	$⊢ \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No$
52		fnfvima	$⊢ (bday Fn No \land \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \subseteq No \land z \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}) \to bday (z) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
53	28 51 52	mp3an12	$⊢ z \in \{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\} \to bday (z) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
54	50 53	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to bday (z) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}]$
55		intss1	$⊢ bday (z) \in bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \to ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \subseteq bday (z)$
56	54 55	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to ⋂ bday [\{y \in No \| (A ≪_{s} \{y\} \land \{y\} ≪_{s} B)\}] \subseteq bday (z)$
57	34 56	eqsstrd	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to bday (A \|_{s} B) \subseteq bday (z)$
58		sseq2	$⊢ bday (z) = x \to (bday (A \|_{s} B) \subseteq bday (z) \leftrightarrow bday (A \|_{s} B) \subseteq x)$
59	58	biimpd	$⊢ bday (z) = x \to (bday (A \|_{s} B) \subseteq bday (z) \to bday (A \|_{s} B) \subseteq x)$
60	59	com12	$⊢ bday (A \|_{s} B) \subseteq bday (z) \to (bday (z) = x \to bday (A \|_{s} B) \subseteq x)$
61	57 60	syl	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to (bday (z) = x \to bday (A \|_{s} B) \subseteq x)$
62	31 61	sylbird	$⊢ (((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \land ((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D))) \to (z bday x \to bday (A \|_{s} B) \subseteq x)$
63	62	ex	$⊢ ((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \to (((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D)) \to (z bday x \to bday (A \|_{s} B) \subseteq x))$
64	63	impd	$⊢ ((A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \land z \in No) \to ((((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D)) \land z bday x) \to bday (A \|_{s} B) \subseteq x)$
65	64	rexlimdva	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (\exists z \in No (((A \cup C) ≪_{s} \{z\} \land \{z\} ≪_{s} (B \cup D)) \land z bday x) \to bday (A \|_{s} B) \subseteq x)$
66	26 65	syl5bi	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (x \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \to bday (A \|_{s} B) \subseteq x)$
67	66	ralrimiv	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to \forall x \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] bday (A \|_{s} B) \subseteq x$
68		ssint	$⊢ bday (A \|_{s} B) \subseteq ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \leftrightarrow \forall x \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] bday (A \|_{s} B) \subseteq x$
69	67 68	sylibr	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to bday (A \|_{s} B) \subseteq ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]$
70	3	simp1d	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to A \|_{s} B \in No$
71	7 11	jca	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to ((A \cup C) ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} (B \cup D))$
72		sneq	$⊢ y = A \|_{s} B \to \{y\} = \{A \|_{s} B\}$
73	72	breq2d	$⊢ y = A \|_{s} B \to ((A \cup C) ≪_{s} \{y\} \leftrightarrow (A \cup C) ≪_{s} \{A \|_{s} B\})$
74	72	breq1d	$⊢ y = A \|_{s} B \to (\{y\} ≪_{s} (B \cup D) \leftrightarrow \{A \|_{s} B\} ≪_{s} (B \cup D))$
75	73 74	anbi12d	$⊢ y = A \|_{s} B \to (((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D)) \leftrightarrow ((A \cup C) ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} (B \cup D)))$
76	75	elrab	$⊢ A \|_{s} B \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \leftrightarrow (A \|_{s} B \in No \land ((A \cup C) ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} (B \cup D)))$
77	70 71 76	sylanbrc	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to A \|_{s} B \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}$
78		ssrab2	$⊢ \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \subseteq No$
79		fnfvima	$⊢ (bday Fn No \land \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \subseteq No \land A \|_{s} B \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}) \to bday (A \|_{s} B) \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]$
80	28 78 79	mp3an12	$⊢ A \|_{s} B \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \to bday (A \|_{s} B) \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]$
81	77 80	syl	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to bday (A \|_{s} B) \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]$
82		intss1	$⊢ bday (A \|_{s} B) \in bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \to ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \subseteq bday (A \|_{s} B)$
83	81 82	syl	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \subseteq bday (A \|_{s} B)$
84	69 83	eqssd	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to bday (A \|_{s} B) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]$
85		conway	$⊢ (A \cup C) ≪_{s} (B \cup D) \to \exists! x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]$
86	16 85	syl	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to \exists! x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]$
87		fveqeq2	$⊢ x = A \|_{s} B \to (bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \leftrightarrow bday (A \|_{s} B) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}])$
88	87	riota2	$⊢ (A \|_{s} B \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \land \exists! x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]) \to (bday (A \|_{s} B) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \leftrightarrow (ι x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \| bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]) = A \|_{s} B)$
89	77 86 88	syl2anc	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (bday (A \|_{s} B) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}] \leftrightarrow (ι x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \| bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]) = A \|_{s} B)$
90	84 89	mpbid	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (ι x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \| bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}]) = A \|_{s} B$
91	90	eqcomd	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to A \|_{s} B = (ι x \in \{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\} \| bday (x) = ⋂ bday [\{y \in No \| ((A \cup C) ≪_{s} \{y\} \land \{y\} ≪_{s} (B \cup D))\}])$
92	18 91	eqtr4d	$⊢ (A ≪_{s} B \land C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to (A \cup C) \|_{s} (B \cup D) = A \|_{s} B$

Metamath Proof Explorer

Theorem scutun12

Proof