noetalem1

Description: Lemma for noeta . Either S or T satisfies the final condition. (Contributed by Scott Fenton, 9-Aug-2024)

	Ref	Expression
Hypotheses	noetalem1.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	noetalem1.2	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	noetalem1.3	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
	noetalem1.4	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
Assertion	noetalem1	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((S \in No \land (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O)) \lor (T \in No \land (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O)))$

Proof

Step	Hyp	Ref	Expression
1		noetalem1.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		noetalem1.2	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
3		noetalem1.3	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
4		noetalem1.4	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
5	2	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
6	5	adantl	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to T \in No$
7		nodmord	$⊢ T \in No \to Ord dom T$
8	6 7	syl	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to Ord dom T$
9	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
10	9	adantr	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to S \in No$
11		nodmord	$⊢ S \in No \to Ord dom S$
12	10 11	syl	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to Ord dom S$
13		ordtri2or2	$⊢ (Ord dom T \land Ord dom S) \to (dom T \subseteq dom S \lor dom S \subseteq dom T)$
14	8 12 13	syl2anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to (dom T \subseteq dom S \lor dom S \subseteq dom T)$
15		ssequn2	$⊢ dom T \subseteq dom S \leftrightarrow dom S \cup dom T = dom S$
16		ssequn1	$⊢ dom S \subseteq dom T \leftrightarrow dom S \cup dom T = dom T$
17	15 16	orbi12i	$⊢ (dom T \subseteq dom S \lor dom S \subseteq dom T) \leftrightarrow (dom S \cup dom T = dom S \lor dom S \cup dom T = dom T)$
18	14 17	sylib	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to (dom S \cup dom T = dom S \lor dom S \cup dom T = dom T)$
19	18	3adant3	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to (dom S \cup dom T = dom S \lor dom S \cup dom T = dom T)$
20		simplll	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to A \subseteq No$
21		simpllr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to A \in V$
22		simplrr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to B \in V$
23		simpr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to a \in A$
24	1 3	noetasuplem3	$⊢ ((A \subseteq No \land A \in V \land B \in V) \land a \in A) \to a <_{s} Z$
25	20 21 22 23 24	syl31anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to a <_{s} Z$
26	25	ralrimiva	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to \forall a \in A a <_{s} Z$
27	26	3adant3	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to \forall a \in A a <_{s} Z$
28	1 3	noetasuplem4	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to \forall b \in B Z <_{s} b$
29	27 28	jca	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to (\forall a \in A a <_{s} Z \land \forall b \in B Z <_{s} b)$
30	29	adantr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom S) \to (\forall a \in A a <_{s} Z \land \forall b \in B Z <_{s} b)$
31		simp1l	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to A \subseteq No$
32		simp1r	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to A \in V$
33		simp2r	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to B \in V$
34	1 3	noetasuplem1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to Z \in No$
35	31 32 33 34	syl3anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to Z \in No$
36	1 2	nosupinfsep	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land Z \in No) \to ((\forall a \in A a <_{s} Z \land \forall b \in B Z <_{s} b) \leftrightarrow (\forall a \in A a <_{s} ({Z ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({Z ↾}_{(dom S \cup dom T)}) <_{s} b))$
37	35 36	syld3an3	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to ((\forall a \in A a <_{s} Z \land \forall b \in B Z <_{s} b) \leftrightarrow (\forall a \in A a <_{s} ({Z ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({Z ↾}_{(dom S \cup dom T)}) <_{s} b))$
38	37	adantr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom S) \to ((\forall a \in A a <_{s} Z \land \forall b \in B Z <_{s} b) \leftrightarrow (\forall a \in A a <_{s} ({Z ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({Z ↾}_{(dom S \cup dom T)}) <_{s} b))$
39		simpr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to dom S \cup dom T = dom S$
40	39	reseq2d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to {Z ↾}_{(dom S \cup dom T)} = {Z ↾}_{dom S}$
41		simplll	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to A \subseteq No$
42		simpllr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to A \in V$
43		simplrr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to B \in V$
44	1 3	noetasuplem2	$⊢ (A \subseteq No \land A \in V \land B \in V) \to {Z ↾}_{dom S} = S$
45	41 42 43 44	syl3anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to {Z ↾}_{dom S} = S$
46	40 45	eqtrd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to {Z ↾}_{(dom S \cup dom T)} = S$
47	46	breq2d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to (a <_{s} ({Z ↾}_{(dom S \cup dom T)}) \leftrightarrow a <_{s} S)$
48	47	ralbidv	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to (\forall a \in A a <_{s} ({Z ↾}_{(dom S \cup dom T)}) \leftrightarrow \forall a \in A a <_{s} S)$
49	46	breq1d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to (({Z ↾}_{(dom S \cup dom T)}) <_{s} b \leftrightarrow S <_{s} b)$
50	49	ralbidv	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to (\forall b \in B ({Z ↾}_{(dom S \cup dom T)}) <_{s} b \leftrightarrow \forall b \in B S <_{s} b)$
51	48 50	anbi12d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom S) \to ((\forall a \in A a <_{s} ({Z ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({Z ↾}_{(dom S \cup dom T)}) <_{s} b) \leftrightarrow (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b))$
52	51	3adantl3	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom S) \to ((\forall a \in A a <_{s} ({Z ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({Z ↾}_{(dom S \cup dom T)}) <_{s} b) \leftrightarrow (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b))$
53	38 52	bitrd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom S) \to ((\forall a \in A a <_{s} Z \land \forall b \in B Z <_{s} b) \leftrightarrow (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b))$
54	30 53	mpbid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom S) \to (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b)$
55	54	ex	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to (dom S \cup dom T = dom S \to (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b))$
56	2 4	noetainflem4	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to \forall a \in A a <_{s} W$
57		simpllr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to A \in V$
58		simplrl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to B \subseteq No$
59		simplrr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to B \in V$
60		simpr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to b \in B$
61	2 4	noetainflem3	$⊢ ((A \in V \land B \subseteq No \land B \in V) \land b \in B) \to W <_{s} b$
62	57 58 59 60 61	syl31anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to W <_{s} b$
63	62	ralrimiva	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to \forall b \in B W <_{s} b$
64	63	3adant3	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to \forall b \in B W <_{s} b$
65	56 64	jca	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to (\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b)$
66	65	adantr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to (\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b)$
67		simpl1	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to (A \subseteq No \land A \in V)$
68		simpl2l	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to B \subseteq No$
69		simpl2r	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to B \in V$
70		simpl1r	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to A \in V$
71	2 4	noetainflem1	$⊢ (A \in V \land B \subseteq No \land B \in V) \to W \in No$
72	70 68 69 71	syl3anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to W \in No$
73	1 2	nosupinfsep	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to ((\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b) \leftrightarrow (\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b))$
74	67 68 69 72 73	syl121anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to ((\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b) \leftrightarrow (\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b))$
75		simpr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to dom S \cup dom T = dom T$
76	75	reseq2d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to {W ↾}_{(dom S \cup dom T)} = {W ↾}_{dom T}$
77		simplr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to (B \subseteq No \land B \in V)$
78	2 4	noetainflem2	$⊢ (B \subseteq No \land B \in V) \to {W ↾}_{dom T} = T$
79	77 78	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to {W ↾}_{dom T} = T$
80	76 79	eqtrd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to {W ↾}_{(dom S \cup dom T)} = T$
81	80	breq2d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to (a <_{s} ({W ↾}_{(dom S \cup dom T)}) \leftrightarrow a <_{s} T)$
82	81	ralbidv	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to (\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \leftrightarrow \forall a \in A a <_{s} T)$
83	80	breq1d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to (({W ↾}_{(dom S \cup dom T)}) <_{s} b \leftrightarrow T <_{s} b)$
84	83	ralbidv	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to (\forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b \leftrightarrow \forall b \in B T <_{s} b)$
85	82 84	anbi12d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land dom S \cup dom T = dom T) \to ((\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b) \leftrightarrow (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b))$
86	85	3adantl3	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to ((\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b) \leftrightarrow (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b))$
87	74 86	bitrd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to ((\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b) \leftrightarrow (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b))$
88	66 87	mpbid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land dom S \cup dom T = dom T) \to (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b)$
89	88	ex	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to (dom S \cup dom T = dom T \to (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b))$
90	55 89	orim12d	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to ((dom S \cup dom T = dom S \lor dom S \cup dom T = dom T) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \lor (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b)))$
91	19 90	mpd	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \lor (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b))$
92	91	adantr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \lor (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b))$
93		simpll	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to (A \subseteq No \land A \in V)$
94		simprl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to O \in On$
95		ssun1	$⊢ A \subseteq A \cup B$
96		imass2	$⊢ A \subseteq A \cup B \to bday [A] \subseteq bday [A \cup B]$
97	95 96	ax-mp	$⊢ bday [A] \subseteq bday [A \cup B]$
98		simprr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to bday [A \cup B] \subseteq O$
99	97 98	sstrid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to bday [A] \subseteq O$
100	1	nosupbday	$⊢ ((A \subseteq No \land A \in V) \land (O \in On \land bday [A] \subseteq O)) \to bday (S) \subseteq O$
101	93 94 99 100	syl12anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to bday (S) \subseteq O$
102	101	a1d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \to bday (S) \subseteq O)$
103	102	ancld	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \land bday (S) \subseteq O))$
104		df-3an	$⊢ (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O) \leftrightarrow ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \land bday (S) \subseteq O)$
105	103 104	imbitrrdi	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \to (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O))$
106	93 9	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to S \in No$
107	105 106	jctild	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \to (S \in No \land (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O)))$
108		simplr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to (B \subseteq No \land B \in V)$
109		ssun2	$⊢ B \subseteq A \cup B$
110		imass2	$⊢ B \subseteq A \cup B \to bday [B] \subseteq bday [A \cup B]$
111	109 110	ax-mp	$⊢ bday [B] \subseteq bday [A \cup B]$
112	111 98	sstrid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to bday [B] \subseteq O$
113	2	noinfbday	$⊢ ((B \subseteq No \land B \in V) \land (O \in On \land bday [B] \subseteq O)) \to bday (T) \subseteq O$
114	108 94 112 113	syl12anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to bday (T) \subseteq O$
115	114	a1d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b) \to bday (T) \subseteq O)$
116	115	ancld	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b) \to ((\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b) \land bday (T) \subseteq O))$
117		df-3an	$⊢ (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O) \leftrightarrow ((\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b) \land bday (T) \subseteq O)$
118	116 117	imbitrrdi	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b) \to (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O))$
119	108 5	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to T \in No$
120	118 119	jctild	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b) \to (T \in No \land (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O)))$
121	107 120	orim12d	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (O \in On \land bday [A \cup B] \subseteq O)) \to (((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \lor (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b)) \to ((S \in No \land (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O)) \lor (T \in No \land (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O))))$
122	121	3adantl3	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land (O \in On \land bday [A \cup B] \subseteq O)) \to (((\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b) \lor (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b)) \to ((S \in No \land (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O)) \lor (T \in No \land (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O))))$
123	92 122	mpd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \land (O \in On \land bday [A \cup B] \subseteq O)) \to ((S \in No \land (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O)) \lor (T \in No \land (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O)))$

Metamath Proof Explorer

Theorem noetalem1

Proof