noetalem2

Description: Lemma for noeta . The full statement of the theorem with hypotheses in place. (Contributed by Scott Fenton, 10-Aug-2024)

	Ref	Expression
Hypotheses	noetalem2.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))))$
	noetalem2.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))))$
Assertion	noetalem2	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall a \in A \forall b \in B a <_{s} b) \land (O \in On \land bday [A \cup B] \subseteq O)) \to \exists c \in No (\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O)$

Proof

Step	Hyp	Ref	Expression
1		noetalem2.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		noetalem2.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		elex	$⊢ A \in V \to A \in V$
4	3	anim2i	$⊢ (A \subseteq No \land A \in V) \to (A \subseteq No \land A \in V)$
5		elex	$⊢ B \in W \to B \in V$
6	5	anim2i	$⊢ (B \subseteq No \land B \in W) \to (B \subseteq No \land B \in V)$
7		id	$⊢ \forall a \in A \forall b \in B a <_{s} b \to \forall a \in A \forall b \in B a <_{s} b$
8	4 6 7	3anim123i	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall a \in A \forall b \in B a <_{s} b) \to ((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)$
9		eqid	$⊢ S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
10		eqid	$⊢ T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
11	1 2 9 10	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)))$
12		breq2	$⊢ c = S \to (a <_{s} c \leftrightarrow a <_{s} S)$
13	12	ralbidv	$⊢ c = S \to (\forall a \in A a <_{s} c \leftrightarrow \forall a \in A a <_{s} S)$
14		breq1	$⊢ c = S \to (c <_{s} b \leftrightarrow S <_{s} b)$
15	14	ralbidv	$⊢ c = S \to (\forall b \in B c <_{s} b \leftrightarrow \forall b \in B S <_{s} b)$
16		fveq2	$⊢ c = S \to bday (c) = bday (S)$
17	16	sseq1d	$⊢ c = S \to (bday (c) \subseteq O \leftrightarrow bday (S) \subseteq O)$
18	13 15 17	3anbi123d	$⊢ c = S \to ((\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O) \leftrightarrow (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O))$
19	18	rspcev	$⊢ (S \in No \land (\forall a \in A a <_{s} S \land \forall b \in B S <_{s} b \land bday (S) \subseteq O)) \to \exists c \in No (\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O)$
20		breq2	$⊢ c = T \to (a <_{s} c \leftrightarrow a <_{s} T)$
21	20	ralbidv	$⊢ c = T \to (\forall a \in A a <_{s} c \leftrightarrow \forall a \in A a <_{s} T)$
22		breq1	$⊢ c = T \to (c <_{s} b \leftrightarrow T <_{s} b)$
23	22	ralbidv	$⊢ c = T \to (\forall b \in B c <_{s} b \leftrightarrow \forall b \in B T <_{s} b)$
24		fveq2	$⊢ c = T \to bday (c) = bday (T)$
25	24	sseq1d	$⊢ c = T \to (bday (c) \subseteq O \leftrightarrow bday (T) \subseteq O)$
26	21 23 25	3anbi123d	$⊢ c = T \to ((\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O) \leftrightarrow (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O))$
27	26	rspcev	$⊢ (T \in No \land (\forall a \in A a <_{s} T \land \forall b \in B T <_{s} b \land bday (T) \subseteq O)) \to \exists c \in No (\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O)$
28	19 27	jaoi	$⊢ ((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))) \to \exists c \in No (\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O)$
29	11 28	syl	$⊢ (((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 \exists c \in No (\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O)$
30	8 29	sylan	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in W) \land \forall a \in A \forall b \in B a <_{s} b) \land (O \in On \land bday [A \cup B] \subseteq O)) \to \exists c \in No (\forall a \in A a <_{s} c \land \forall b \in B c <_{s} b \land bday (c) \subseteq O)$

Metamath Proof Explorer

Theorem noetalem2

Proof