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

Metamath Proof Explorer

Theorem noetainflem2

Proof