noetainflem2

Description: Lemma for noeta . The restriction of W to the domain of T is T . (Contributed by Scott Fenton, 9-Aug-2024)

	Ref	Expression
Hypotheses	noetainflem.1	$⊢ 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))))$
	noetainflem.2	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
Assertion	noetainflem2	$⊢ (B \subseteq No \land B \in V) \to {W ↾}_{dom T} = T$

Proof

Step	Hyp	Ref	Expression
1		noetainflem.1	$⊢ 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))))$
2		noetainflem.2	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
3	2	reseq1i	$⊢ {W ↾}_{dom T} = {(T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})) ↾}_{dom T}$
4		resundir	$⊢ {(T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})) ↾}_{dom T} = ({T ↾}_{dom T}) \cup ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T})$
5	3 4	eqtri	$⊢ {W ↾}_{dom T} = ({T ↾}_{dom T}) \cup ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T})$
6	1	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
7		nofun	$⊢ T \in No \to Fun T$
8	6 7	syl	$⊢ (B \subseteq No \land B \in V) \to Fun T$
9		funrel	$⊢ Fun T \to Rel T$
10		resdm	$⊢ Rel T \to {T ↾}_{dom T} = T$
11	8 9 10	3syl	$⊢ (B \subseteq No \land B \in V) \to {T ↾}_{dom T} = T$
12		dmres	$⊢ dom ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T}) = dom T \cap dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
13		2oex	$⊢ 2_{𝑜} \in V$
14	13	snnz	$⊢ \{2_{𝑜}\} \neq \emptyset$
15		dmxp	$⊢ \{2_{𝑜}\} \neq \emptyset \to dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = suc ⋃ bday [A] ∖ dom T$
16	14 15	ax-mp	$⊢ dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = suc ⋃ bday [A] ∖ dom T$
17	16	ineq2i	$⊢ dom T \cap dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = dom T \cap (suc ⋃ bday [A] ∖ dom T)$
18		disjdif	$⊢ dom T \cap (suc ⋃ bday [A] ∖ dom T) = \emptyset$
19	17 18	eqtri	$⊢ dom T \cap dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = \emptyset$
20	12 19	eqtri	$⊢ dom ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T}) = \emptyset$
21		relres	$⊢ Rel ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T})$
22		reldm0	$⊢ Rel ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T}) \to ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T} = \emptyset \leftrightarrow dom ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T}) = \emptyset)$
23	21 22	ax-mp	$⊢ {((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T} = \emptyset \leftrightarrow dom ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T}) = \emptyset$
24	20 23	mpbir	$⊢ {((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T} = \emptyset$
25	24	a1i	$⊢ (B \subseteq No \land B \in V) \to {((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T} = \emptyset$
26	11 25	uneq12d	$⊢ (B \subseteq No \land B \in V) \to ({T ↾}_{dom T}) \cup ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T}) = T \cup \emptyset$
27		un0	$⊢ T \cup \emptyset = T$
28	26 27	eqtrdi	$⊢ (B \subseteq No \land B \in V) \to ({T ↾}_{dom T}) \cup ({((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) ↾}_{dom T}) = T$
29	5 28	syl5eq	$⊢ (B \subseteq No \land B \in V) \to {W ↾}_{dom T} = T$

Metamath Proof Explorer

Theorem noetainflem2

Proof