noinfbnd2lem1

Description: Bounding law from below when a set of surreals has a minimum. (Contributed by Scott Fenton, 9-Aug-2024)

		Ref	Expression
	Assertion	noinfbnd2lem1	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U})$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ b = U \to (Z <_{s} b \leftrightarrow Z <_{s} U)$
2		simp3	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to \forall b \in B Z <_{s} b$
3		simp1l	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to U \in B$
4	1 2 3	rspcdva	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to Z <_{s} U$
5		simpl21	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to B \subseteq No$
6		simpl1l	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to U \in B$
7	5 6	sseldd	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to U \in No$
8		nodmon	$⊢ U \in No \to dom U \in On$
9	7 8	syl	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to dom U \in On$
10		onelon	$⊢ (dom U \in On \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \in On$
11	9 10	sylan	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \in On$
12		simpr	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}$
13		simplr	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U$
14	9	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to dom U \in On$
15	14	adantr	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to dom U \in On$
16		ontr1	$⊢ dom U \in On \to ((q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to q \in dom U)$
17	15 16	syl	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to ((q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to q \in dom U)$
18	12 13 17	mp2and	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to q \in dom U$
19	18	fvresd	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to ({Z ↾}_{dom U}) (q) = Z (q)$
20		onelon	$⊢ (⋂ \{x \in On \| U (x) \neq Z (x)\} \in On \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to q \in On$
21	11 20	sylan	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to q \in On$
22		fveq2	$⊢ x = q \to U (x) = U (q)$
23		fveq2	$⊢ x = q \to Z (x) = Z (q)$
24	22 23	neeq12d	$⊢ x = q \to (U (x) \neq Z (x) \leftrightarrow U (q) \neq Z (q))$
25	24	onnminsb	$⊢ q \in On \to (q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} \to \neg U (q) \neq Z (q))$
26	21 12 25	sylc	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to \neg U (q) \neq Z (q)$
27		df-ne	$⊢ U (q) \neq Z (q) \leftrightarrow \neg U (q) = Z (q)$
28	27	con2bii	$⊢ U (q) = Z (q) \leftrightarrow \neg U (q) \neq Z (q)$
29	26 28	sylibr	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to U (q) = Z (q)$
30	19 29	eqtr4d	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \land q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}) \to ({Z ↾}_{dom U}) (q) = U (q)$
31	30	ralrimiva	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to \forall q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} ({Z ↾}_{dom U}) (q) = U (q)$
32		simpr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U$
33	32	fvresd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ({Z ↾}_{dom U}) (⋂ \{x \in On \| U (x) \neq Z (x)\}) = Z (⋂ \{x \in On \| U (x) \neq Z (x)\})$
34		simplr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to Z <_{s} U$
35		simpl23	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Z \in No$
36	7	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to U \in No$
37		sltval2	$⊢ (Z \in No \land U \in No) \to (Z <_{s} U \leftrightarrow Z (⋂ \{x \in On \| Z (x) \neq U (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| Z (x) \neq U (x)\}))$
38	35 36 37	syl2an2r	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to (Z <_{s} U \leftrightarrow Z (⋂ \{x \in On \| Z (x) \neq U (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| Z (x) \neq U (x)\}))$
39	34 38	mpbid	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to Z (⋂ \{x \in On \| Z (x) \neq U (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| Z (x) \neq U (x)\})$
40		necom	$⊢ U (x) \neq Z (x) \leftrightarrow Z (x) \neq U (x)$
41	40	rabbii	$⊢ \{x \in On \| U (x) \neq Z (x)\} = \{x \in On \| Z (x) \neq U (x)\}$
42	41	inteqi	$⊢ ⋂ \{x \in On \| U (x) \neq Z (x)\} = ⋂ \{x \in On \| Z (x) \neq U (x)\}$
43	42	fveq2i	$⊢ Z (⋂ \{x \in On \| U (x) \neq Z (x)\}) = Z (⋂ \{x \in On \| Z (x) \neq U (x)\})$
44	42	fveq2i	$⊢ U (⋂ \{x \in On \| U (x) \neq Z (x)\}) = U (⋂ \{x \in On \| Z (x) \neq U (x)\})$
45	39 43 44	3brtr4g	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to Z (⋂ \{x \in On \| U (x) \neq Z (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| U (x) \neq Z (x)\})$
46	33 45	eqbrtrd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ({Z ↾}_{dom U}) (⋂ \{x \in On \| U (x) \neq Z (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| U (x) \neq Z (x)\})$
47		raleq	$⊢ p = ⋂ \{x \in On \| U (x) \neq Z (x)\} \to (\forall q \in p ({Z ↾}_{dom U}) (q) = U (q) \leftrightarrow \forall q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} ({Z ↾}_{dom U}) (q) = U (q))$
48		fveq2	$⊢ p = ⋂ \{x \in On \| U (x) \neq Z (x)\} \to ({Z ↾}_{dom U}) (p) = ({Z ↾}_{dom U}) (⋂ \{x \in On \| U (x) \neq Z (x)\})$
49		fveq2	$⊢ p = ⋂ \{x \in On \| U (x) \neq Z (x)\} \to U (p) = U (⋂ \{x \in On \| U (x) \neq Z (x)\})$
50	48 49	breq12d	$⊢ p = ⋂ \{x \in On \| U (x) \neq Z (x)\} \to (({Z ↾}_{dom U}) (p) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (p) \leftrightarrow ({Z ↾}_{dom U}) (⋂ \{x \in On \| U (x) \neq Z (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| U (x) \neq Z (x)\}))$
51	47 50	anbi12d	$⊢ p = ⋂ \{x \in On \| U (x) \neq Z (x)\} \to ((\forall q \in p ({Z ↾}_{dom U}) (q) = U (q) \land ({Z ↾}_{dom U}) (p) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (p)) \leftrightarrow (\forall q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} ({Z ↾}_{dom U}) (q) = U (q) \land ({Z ↾}_{dom U}) (⋂ \{x \in On \| U (x) \neq Z (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| U (x) \neq Z (x)\})))$
52	51	rspcev	$⊢ (⋂ \{x \in On \| U (x) \neq Z (x)\} \in On \land (\forall q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} ({Z ↾}_{dom U}) (q) = U (q) \land ({Z ↾}_{dom U}) (⋂ \{x \in On \| U (x) \neq Z (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| U (x) \neq Z (x)\}))) \to \exists p \in On (\forall q \in p ({Z ↾}_{dom U}) (q) = U (q) \land ({Z ↾}_{dom U}) (p) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (p))$
53	11 31 46 52	syl12anc	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to \exists p \in On (\forall q \in p ({Z ↾}_{dom U}) (q) = U (q) \land ({Z ↾}_{dom U}) (p) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (p))$
54		noreson	$⊢ (Z \in No \land dom U \in On) \to {Z ↾}_{dom U} \in No$
55	35 9 54	syl2anc	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to {Z ↾}_{dom U} \in No$
56		sltval	$⊢ ({Z ↾}_{dom U} \in No \land U \in No) \to (({Z ↾}_{dom U}) <_{s} U \leftrightarrow \exists p \in On (\forall q \in p ({Z ↾}_{dom U}) (q) = U (q) \land ({Z ↾}_{dom U}) (p) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (p)))$
57	55 36 56	syl2an2r	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to (({Z ↾}_{dom U}) <_{s} U \leftrightarrow \exists p \in On (\forall q \in p ({Z ↾}_{dom U}) (q) = U (q) \land ({Z ↾}_{dom U}) (p) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (p)))$
58	53 57	mpbird	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ({Z ↾}_{dom U}) <_{s} U$
59		sssucid	$⊢ dom U \subseteq suc dom U$
60		resabs1	$⊢ dom U \subseteq suc dom U \to {({Z ↾}_{suc dom U}) ↾}_{dom U} = {Z ↾}_{dom U}$
61	59 60	mp1i	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to {({Z ↾}_{suc dom U}) ↾}_{dom U} = {Z ↾}_{dom U}$
62		resundir	$⊢ {(U \cup \{⟨dom U, 1_{𝑜}⟩\}) ↾}_{dom U} = ({U ↾}_{dom U}) \cup ({\{⟨dom U, 1_{𝑜}⟩\} ↾}_{dom U})$
63		nofun	$⊢ U \in No \to Fun U$
64	7 63	syl	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Fun U$
65		funrel	$⊢ Fun U \to Rel U$
66	64 65	syl	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Rel U$
67	66	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to Rel U$
68		resdm	$⊢ Rel U \to {U ↾}_{dom U} = U$
69	67 68	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to {U ↾}_{dom U} = U$
70		nodmord	$⊢ U \in No \to Ord dom U$
71	7 70	syl	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Ord dom U$
72	71	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to Ord dom U$
73		ordirr	$⊢ Ord dom U \to \neg dom U \in dom U$
74	72 73	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to \neg dom U \in dom U$
75		1oex	$⊢ 1_{𝑜} \in V$
76	75	snres0	$⊢ {\{⟨dom U, 1_{𝑜}⟩\} ↾}_{dom U} = \emptyset \leftrightarrow \neg dom U \in dom U$
77	74 76	sylibr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to {\{⟨dom U, 1_{𝑜}⟩\} ↾}_{dom U} = \emptyset$
78	69 77	uneq12d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ({U ↾}_{dom U}) \cup ({\{⟨dom U, 1_{𝑜}⟩\} ↾}_{dom U}) = U \cup \emptyset$
79		un0	$⊢ U \cup \emptyset = U$
80	78 79	eqtrdi	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ({U ↾}_{dom U}) \cup ({\{⟨dom U, 1_{𝑜}⟩\} ↾}_{dom U}) = U$
81	62 80	eqtrid	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to {(U \cup \{⟨dom U, 1_{𝑜}⟩\}) ↾}_{dom U} = U$
82	58 61 81	3brtr4d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ({({Z ↾}_{suc dom U}) ↾}_{dom U}) <_{s} ({(U \cup \{⟨dom U, 1_{𝑜}⟩\}) ↾}_{dom U})$
83		sucelon	$⊢ dom U \in On \leftrightarrow suc dom U \in On$
84	9 83	sylib	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to suc dom U \in On$
85		noreson	$⊢ (Z \in No \land suc dom U \in On) \to {Z ↾}_{suc dom U} \in No$
86	35 84 85	syl2anc	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to {Z ↾}_{suc dom U} \in No$
87	86	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to {Z ↾}_{suc dom U} \in No$
88	75	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
89	88	noextend	$⊢ U \in No \to U \cup \{⟨dom U, 1_{𝑜}⟩\} \in No$
90	7 89	syl	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to U \cup \{⟨dom U, 1_{𝑜}⟩\} \in No$
91	90	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to U \cup \{⟨dom U, 1_{𝑜}⟩\} \in No$
92		sltres	$⊢ ({Z ↾}_{suc dom U} \in No \land U \cup \{⟨dom U, 1_{𝑜}⟩\} \in No \land dom U \in On) \to (({({Z ↾}_{suc dom U}) ↾}_{dom U}) <_{s} ({(U \cup \{⟨dom U, 1_{𝑜}⟩\}) ↾}_{dom U}) \to ({Z ↾}_{suc dom U}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\}))$
93	87 91 14 92	syl3anc	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to (({({Z ↾}_{suc dom U}) ↾}_{dom U}) <_{s} ({(U \cup \{⟨dom U, 1_{𝑜}⟩\}) ↾}_{dom U}) \to ({Z ↾}_{suc dom U}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\}))$
94	82 93	mpd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to ({Z ↾}_{suc dom U}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\})$
95		sltso	$⊢ <_{s} Or No$
96		soasym	$⊢ (<_{s} Or No \land ({Z ↾}_{suc dom U} \in No \land U \cup \{⟨dom U, 1_{𝑜}⟩\} \in No)) \to (({Z ↾}_{suc dom U}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\}) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U}))$
97	95 96	mpan	$⊢ ({Z ↾}_{suc dom U} \in No \land U \cup \{⟨dom U, 1_{𝑜}⟩\} \in No) \to (({Z ↾}_{suc dom U}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\}) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U}))$
98	86 91 97	syl2an2r	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to (({Z ↾}_{suc dom U}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\}) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U}))$
99	94 98	mpd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U})$
100		sonr	$⊢ (<_{s} Or No \land U \cup \{⟨dom U, 1_{𝑜}⟩\} \in No) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\})$
101	95 90 100	sylancr	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\})$
102	101	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\})$
103		df-suc	$⊢ suc dom U = dom U \cup \{dom U\}$
104	103	reseq2i	$⊢ {Z ↾}_{suc dom U} = {Z ↾}_{(dom U \cup \{dom U\})}$
105		resundi	$⊢ {Z ↾}_{(dom U \cup \{dom U\})} = ({Z ↾}_{dom U}) \cup ({Z ↾}_{\{dom U\}})$
106	104 105	eqtri	$⊢ {Z ↾}_{suc dom U} = ({Z ↾}_{dom U}) \cup ({Z ↾}_{\{dom U\}})$
107		dmres	$⊢ dom ({Z ↾}_{dom U}) = dom U \cap dom Z$
108	42	eqeq1i	$⊢ ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U \leftrightarrow ⋂ \{x \in On \| Z (x) \neq U (x)\} = dom U$
109	108	biimpi	$⊢ ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U \to ⋂ \{x \in On \| Z (x) \neq U (x)\} = dom U$
110	109	adantl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ⋂ \{x \in On \| Z (x) \neq U (x)\} = dom U$
111	35	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Z \in No$
112	7	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to U \in No$
113		simp23	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to Z \in No$
114		sonr	$⊢ (<_{s} Or No \land Z \in No) \to \neg Z <_{s} Z$
115	95 113 114	sylancr	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to \neg Z <_{s} Z$
116		breq2	$⊢ U = Z \to (Z <_{s} U \leftrightarrow Z <_{s} Z)$
117	116	notbid	$⊢ U = Z \to (\neg Z <_{s} U \leftrightarrow \neg Z <_{s} Z)$
118	115 117	syl5ibrcom	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to (U = Z \to \neg Z <_{s} U)$
119	118	necon2ad	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to (Z <_{s} U \to U \neq Z)$
120	119	imp	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to U \neq Z$
121	120	necomd	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Z \neq U$
122	121	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Z \neq U$
123		nosepssdm	$⊢ (Z \in No \land U \in No \land Z \neq U) \to ⋂ \{x \in On \| Z (x) \neq U (x)\} \subseteq dom Z$
124	111 112 122 123	syl3anc	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ⋂ \{x \in On \| Z (x) \neq U (x)\} \subseteq dom Z$
125	110 124	eqsstrrd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to dom U \subseteq dom Z$
126		df-ss	$⊢ dom U \subseteq dom Z \leftrightarrow dom U \cap dom Z = dom U$
127	125 126	sylib	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to dom U \cap dom Z = dom U$
128	107 127	eqtrid	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to dom ({Z ↾}_{dom U}) = dom U$
129	128	eleq2d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to (q \in dom ({Z ↾}_{dom U}) \leftrightarrow q \in dom U)$
130		simpr	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \land q \in dom U) \to q \in dom U$
131	130	fvresd	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \land q \in dom U) \to ({Z ↾}_{dom U}) (q) = Z (q)$
132	112 8	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to dom U \in On$
133		onelon	$⊢ (dom U \in On \land q \in dom U) \to q \in On$
134	132 133	sylan	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \land q \in dom U) \to q \in On$
135		simpr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U$
136	135	eleq2d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to (q \in ⋂ \{x \in On \| U (x) \neq Z (x)\} \leftrightarrow q \in dom U)$
137	136	biimpar	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \land q \in dom U) \to q \in ⋂ \{x \in On \| U (x) \neq Z (x)\}$
138	134 137 25	sylc	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \land q \in dom U) \to \neg U (q) \neq Z (q)$
139		nesym	$⊢ U (q) \neq Z (q) \leftrightarrow \neg Z (q) = U (q)$
140	139	con2bii	$⊢ Z (q) = U (q) \leftrightarrow \neg U (q) \neq Z (q)$
141	138 140	sylibr	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \land q \in dom U) \to Z (q) = U (q)$
142	131 141	eqtrd	$⊢ (((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \land q \in dom U) \to ({Z ↾}_{dom U}) (q) = U (q)$
143	142	ex	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to (q \in dom U \to ({Z ↾}_{dom U}) (q) = U (q))$
144	129 143	sylbid	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to (q \in dom ({Z ↾}_{dom U}) \to ({Z ↾}_{dom U}) (q) = U (q))$
145	144	ralrimiv	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to \forall q \in dom ({Z ↾}_{dom U}) ({Z ↾}_{dom U}) (q) = U (q)$
146		nofun	$⊢ Z \in No \to Fun Z$
147	111 146	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Fun Z$
148	147	funresd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Fun ({Z ↾}_{dom U})$
149	64	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Fun U$
150		eqfunfv	$⊢ (Fun ({Z ↾}_{dom U}) \land Fun U) \to ({Z ↾}_{dom U} = U \leftrightarrow (dom ({Z ↾}_{dom U}) = dom U \land \forall q \in dom ({Z ↾}_{dom U}) ({Z ↾}_{dom U}) (q) = U (q)))$
151	148 149 150	syl2anc	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ({Z ↾}_{dom U} = U \leftrightarrow (dom ({Z ↾}_{dom U}) = dom U \land \forall q \in dom ({Z ↾}_{dom U}) ({Z ↾}_{dom U}) (q) = U (q)))$
152	128 145 151	mpbir2and	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to {Z ↾}_{dom U} = U$
153	35 146	syl	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Fun Z$
154	153	funfnd	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Z Fn dom Z$
155	112 70	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Ord dom U$
156	155 73	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to \neg dom U \in dom U$
157		ndmfv	$⊢ \neg dom U \in dom U \to U (dom U) = \emptyset$
158		2on0	$⊢ 2_{𝑜} \neq \emptyset$
159	158	necomi	$⊢ \emptyset \neq 2_{𝑜}$
160		neeq1	$⊢ U (dom U) = \emptyset \to (U (dom U) \neq 2_{𝑜} \leftrightarrow \emptyset \neq 2_{𝑜})$
161	159 160	mpbiri	$⊢ U (dom U) = \emptyset \to U (dom U) \neq 2_{𝑜}$
162	161	neneqd	$⊢ U (dom U) = \emptyset \to \neg U (dom U) = 2_{𝑜}$
163	157 162	syl	$⊢ \neg dom U \in dom U \to \neg U (dom U) = 2_{𝑜}$
164	156 163	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to \neg U (dom U) = 2_{𝑜}$
165	164	intnand	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to \neg (Z (dom U) = \emptyset \land U (dom U) = 2_{𝑜})$
166		simpr	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Z <_{s} U$
167	35 7 37	syl2anc	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to (Z <_{s} U \leftrightarrow Z (⋂ \{x \in On \| Z (x) \neq U (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| Z (x) \neq U (x)\}))$
168	166 167	mpbid	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to Z (⋂ \{x \in On \| Z (x) \neq U (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| Z (x) \neq U (x)\})$
169	168	adantr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Z (⋂ \{x \in On \| Z (x) \neq U (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (⋂ \{x \in On \| Z (x) \neq U (x)\})$
170	110	fveq2d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Z (⋂ \{x \in On \| Z (x) \neq U (x)\}) = Z (dom U)$
171	110	fveq2d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to U (⋂ \{x \in On \| Z (x) \neq U (x)\}) = U (dom U)$
172	169 170 171	3brtr3d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Z (dom U) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (dom U)$
173		fvex	$⊢ Z (dom U) \in V$
174		fvex	$⊢ U (dom U) \in V$
175	173 174	brtp	$⊢ Z (dom U) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} U (dom U) \leftrightarrow ((Z (dom U) = 1_{𝑜} \land U (dom U) = \emptyset) \lor (Z (dom U) = 1_{𝑜} \land U (dom U) = 2_{𝑜}) \lor (Z (dom U) = \emptyset \land U (dom U) = 2_{𝑜}))$
176	172 175	sylib	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ((Z (dom U) = 1_{𝑜} \land U (dom U) = \emptyset) \lor (Z (dom U) = 1_{𝑜} \land U (dom U) = 2_{𝑜}) \lor (Z (dom U) = \emptyset \land U (dom U) = 2_{𝑜}))$
177		3orel3	$⊢ \neg (Z (dom U) = \emptyset \land U (dom U) = 2_{𝑜}) \to (((Z (dom U) = 1_{𝑜} \land U (dom U) = \emptyset) \lor (Z (dom U) = 1_{𝑜} \land U (dom U) = 2_{𝑜}) \lor (Z (dom U) = \emptyset \land U (dom U) = 2_{𝑜})) \to ((Z (dom U) = 1_{𝑜} \land U (dom U) = \emptyset) \lor (Z (dom U) = 1_{𝑜} \land U (dom U) = 2_{𝑜})))$
178	165 176 177	sylc	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ((Z (dom U) = 1_{𝑜} \land U (dom U) = \emptyset) \lor (Z (dom U) = 1_{𝑜} \land U (dom U) = 2_{𝑜}))$
179		andi	$⊢ (Z (dom U) = 1_{𝑜} \land (U (dom U) = \emptyset \lor U (dom U) = 2_{𝑜})) \leftrightarrow ((Z (dom U) = 1_{𝑜} \land U (dom U) = \emptyset) \lor (Z (dom U) = 1_{𝑜} \land U (dom U) = 2_{𝑜}))$
180	178 179	sylibr	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to (Z (dom U) = 1_{𝑜} \land (U (dom U) = \emptyset \lor U (dom U) = 2_{𝑜}))$
181	180	simpld	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to Z (dom U) = 1_{𝑜}$
182		ndmfv	$⊢ \neg dom U \in dom Z \to Z (dom U) = \emptyset$
183		1n0	$⊢ 1_{𝑜} \neq \emptyset$
184	183	necomi	$⊢ \emptyset \neq 1_{𝑜}$
185		neeq1	$⊢ Z (dom U) = \emptyset \to (Z (dom U) \neq 1_{𝑜} \leftrightarrow \emptyset \neq 1_{𝑜})$
186	184 185	mpbiri	$⊢ Z (dom U) = \emptyset \to Z (dom U) \neq 1_{𝑜}$
187	186	neneqd	$⊢ Z (dom U) = \emptyset \to \neg Z (dom U) = 1_{𝑜}$
188	182 187	syl	$⊢ \neg dom U \in dom Z \to \neg Z (dom U) = 1_{𝑜}$
189	188	con4i	$⊢ Z (dom U) = 1_{𝑜} \to dom U \in dom Z$
190	181 189	syl	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to dom U \in dom Z$
191		fnressn	$⊢ (Z Fn dom Z \land dom U \in dom Z) \to {Z ↾}_{\{dom U\}} = \{⟨dom U, Z (dom U)⟩\}$
192	154 190 191	syl2an2r	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to {Z ↾}_{\{dom U\}} = \{⟨dom U, Z (dom U)⟩\}$
193	181	opeq2d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ⟨dom U, Z (dom U)⟩ = ⟨dom U, 1_{𝑜}⟩$
194	193	sneqd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to \{⟨dom U, Z (dom U)⟩\} = \{⟨dom U, 1_{𝑜}⟩\}$
195	192 194	eqtrd	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to {Z ↾}_{\{dom U\}} = \{⟨dom U, 1_{𝑜}⟩\}$
196	152 195	uneq12d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ({Z ↾}_{dom U}) \cup ({Z ↾}_{\{dom U\}}) = U \cup \{⟨dom U, 1_{𝑜}⟩\}$
197	106 196	eqtrid	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to {Z ↾}_{suc dom U} = U \cup \{⟨dom U, 1_{𝑜}⟩\}$
198	197	breq2d	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to ((U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U}) \leftrightarrow (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} (U \cup \{⟨dom U, 1_{𝑜}⟩\}))$
199	102 198	mtbird	$⊢ ((((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \land ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U})$
200		nosepssdm	$⊢ (U \in No \land Z \in No \land U \neq Z) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \subseteq dom U$
201	7 35 120 200	syl3anc	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \subseteq dom U$
202		nosepon	$⊢ (U \in No \land Z \in No \land U \neq Z) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \in On$
203	7 35 120 202	syl3anc	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \in On$
204		onsseleq	$⊢ (⋂ \{x \in On \| U (x) \neq Z (x)\} \in On \land dom U \in On) \to (⋂ \{x \in On \| U (x) \neq Z (x)\} \subseteq dom U \leftrightarrow (⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U \lor ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U))$
205	203 9 204	syl2anc	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to (⋂ \{x \in On \| U (x) \neq Z (x)\} \subseteq dom U \leftrightarrow (⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U \lor ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U))$
206	201 205	mpbid	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to (⋂ \{x \in On \| U (x) \neq Z (x)\} \in dom U \lor ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U)$
207	99 199 206	mpjaodan	$⊢ (((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \land Z <_{s} U) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U})$
208	4 207	mpdan	$⊢ ((U \in B \land \forall y \in B \neg y <_{s} U) \land (B \subseteq No \land B \in V \land Z \in No) \land \forall b \in B Z <_{s} b) \to \neg (U \cup \{⟨dom U, 1_{𝑜}⟩\}) <_{s} ({Z ↾}_{suc dom U})$

Metamath Proof Explorer

Theorem noinfbnd2lem1

Proof