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		ltsval2	$⊢ (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		ltsval	$⊢ ({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		onsucb	$⊢ 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		ltsres	$⊢ ({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		ltsso	$⊢ <_{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	bilani	$⊢ ((((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$
110	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$
111	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$
112		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$
113		sonr	$⊢ (<_{s} Or No \land Z \in No) \to \neg Z <_{s} Z$
114	95 112 113	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$
115		breq2	$⊢ U = Z \to (Z <_{s} U \leftrightarrow Z <_{s} Z)$
116	115	notbid	$⊢ U = Z \to (\neg Z <_{s} U \leftrightarrow \neg Z <_{s} Z)$
117	114 116	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)$
118	117	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)$
119	118	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$
120	119	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$
121	120	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$
122		nosepssdm	$⊢ (Z \in No \land U \in No \land Z \neq U) \to ⋂ \{x \in On \| Z (x) \neq U (x)\} \subseteq dom Z$
123	110 111 121 122	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$
124	109 123	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$
125		dfss2	$⊢ dom U \subseteq dom Z \leftrightarrow dom U \cap dom Z = dom U$
126	124 125	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$
127	107 126	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$
128	127	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)$
129		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$
130	129	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)$
131	111 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$
132		onelon	$⊢ (dom U \in On \land q \in dom U) \to q \in On$
133	131 132	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$
134		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$
135	134	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)$
136	135	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)\}$
137	133 136 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)$
138		nesym	$⊢ U (q) \neq Z (q) \leftrightarrow \neg Z (q) = U (q)$
139	138	con2bii	$⊢ Z (q) = U (q) \leftrightarrow \neg U (q) \neq Z (q)$
140	137 139	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)$
141	130 140	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)$
142	141	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))$
143	128 142	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))$
144	143	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)$
145		nofun	$⊢ Z \in No \to Fun Z$
146	110 145	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$
147	146	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})$
148	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$
149		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)))$
150	147 148 149	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)))$
151	127 144 150	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$
152	35 145	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$
153	152	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$
154		ndmfv	$⊢ \neg dom U \in dom U \to U (dom U) = \emptyset$
155		2on0	$⊢ 2_{𝑜} \neq \emptyset$
156	155	necomi	$⊢ \emptyset \neq 2_{𝑜}$
157		neeq1	$⊢ U (dom U) = \emptyset \to (U (dom U) \neq 2_{𝑜} \leftrightarrow \emptyset \neq 2_{𝑜})$
158	156 157	mpbiri	$⊢ U (dom U) = \emptyset \to U (dom U) \neq 2_{𝑜}$
159	158	neneqd	$⊢ U (dom U) = \emptyset \to \neg U (dom U) = 2_{𝑜}$
160	154 159	syl	$⊢ \neg dom U \in dom U \to \neg U (dom U) = 2_{𝑜}$
161	111 70 73 160	4syl	$⊢ ((((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_{𝑜}$
162	161	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_{𝑜})$
163		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$
164	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)\}))$
165	163 164	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)\})$
166	165	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)\})$
167	109	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)$
168	109	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)$
169	166 167 168	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)$
170		fvex	$⊢ Z (dom U) \in V$
171		fvex	$⊢ U (dom U) \in V$
172	170 171	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_{𝑜}))$
173	169 172	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_{𝑜}))$
174		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_{𝑜})))$
175	162 173 174	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_{𝑜}))$
176		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_{𝑜}))$
177	175 176	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_{𝑜}))$
178	177	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_{𝑜}$
179		ndmfv	$⊢ \neg dom U \in dom Z \to Z (dom U) = \emptyset$
180		1n0	$⊢ 1_{𝑜} \neq \emptyset$
181	180	necomi	$⊢ \emptyset \neq 1_{𝑜}$
182		neeq1	$⊢ Z (dom U) = \emptyset \to (Z (dom U) \neq 1_{𝑜} \leftrightarrow \emptyset \neq 1_{𝑜})$
183	181 182	mpbiri	$⊢ Z (dom U) = \emptyset \to Z (dom U) \neq 1_{𝑜}$
184	183	neneqd	$⊢ Z (dom U) = \emptyset \to \neg Z (dom U) = 1_{𝑜}$
185	179 184	syl	$⊢ \neg dom U \in dom Z \to \neg Z (dom U) = 1_{𝑜}$
186	185	con4i	$⊢ Z (dom U) = 1_{𝑜} \to dom U \in dom Z$
187	178 186	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$
188		fnressn	$⊢ (Z Fn dom Z \land dom U \in dom Z) \to {Z ↾}_{\{dom U\}} = \{⟨dom U, Z (dom U)⟩\}$
189	153 187 188	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)⟩\}$
190	178	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_{𝑜}⟩$
191	190	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_{𝑜}⟩\}$
192	189 191	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_{𝑜}⟩\}$
193	151 192	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_{𝑜}⟩\}$
194	106 193	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_{𝑜}⟩\}$
195	194	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_{𝑜}⟩\}))$
196	102 195	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})$
197		nosepssdm	$⊢ (U \in No \land Z \in No \land U \neq Z) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \subseteq dom U$
198	7 35 119 197	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$
199		nosepon	$⊢ (U \in No \land Z \in No \land U \neq Z) \to ⋂ \{x \in On \| U (x) \neq Z (x)\} \in On$
200	7 35 119 199	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$
201		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))$
202	200 9 201	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))$
203	198 202	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)$
204	99 196 203	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})$
205	4 204	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