nosupbnd2lem1

Description: Bounding law from above when a set of surreals has a maximum. (Contributed by Scott Fenton, 6-Dec-2021)

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

Proof

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

Metamath Proof Explorer

Theorem nosupbnd2lem1

Proof