noetasuplem2

Description: Lemma for noeta . The restriction of Z to dom S is S . (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

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

Metamath Proof Explorer

Theorem noetasuplem2

Proof