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		ltsso	$⊢ <_{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		ltsval2	$⊢ (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		ltsval	$⊢ (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	eqtrid	$⊢ ((((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	eqtrid	$⊢ ((((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		funrel	$⊢ Fun U \to Rel U$
96		resdm	$⊢ Rel U \to {U ↾}_{dom U} = U$
97	30 94 95 96	4syl	$⊢ ((((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$
98	93 97	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$
99		sssucid	$⊢ dom U \subseteq suc dom U$
100		resabs1	$⊢ dom U \subseteq suc dom U \to {({Z ↾}_{suc dom U}) ↾}_{dom U} = {Z ↾}_{dom U}$
101	99 100	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}$
102	72 98 101	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})$
103	74	elexi	$⊢ 2_{𝑜} \in V$
104	103	prid2	$⊢ 2_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
105	104	noextend	$⊢ U \in No \to U \cup \{⟨dom U, 2_{𝑜}⟩\} \in No$
106	8 105	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$
107	106	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$
108		onsucb	$⊢ dom U \in On \leftrightarrow suc dom U \in On$
109	27 108	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$
110		noreson	$⊢ (Z \in No \land suc dom U \in On) \to {Z ↾}_{suc dom U} \in No$
111	9 109 110	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$
112	111	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$
113		ltsres	$⊢ (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}))$
114	107 112 46 113	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}))$
115	102 114	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})$
116		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_{𝑜}⟩\}))$
117	12 116	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_{𝑜}⟩\}))$
118	107 112 117	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_{𝑜}⟩\}))$
119	115 118	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_{𝑜}⟩\})$
120		df-suc	$⊢ suc dom U = dom U \cup \{dom U\}$
121	120	reseq2i	$⊢ {Z ↾}_{suc dom U} = {Z ↾}_{(dom U \cup \{dom U\})}$
122		resundi	$⊢ {Z ↾}_{(dom U \cup \{dom U\})} = ({Z ↾}_{dom U}) \cup ({Z ↾}_{\{dom U\}})$
123	121 122	eqtri	$⊢ {Z ↾}_{suc dom U} = ({Z ↾}_{dom U}) \cup ({Z ↾}_{\{dom U\}})$
124		dmres	$⊢ dom ({Z ↾}_{dom U}) = dom U \cap dom Z$
125		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$
126		necom	$⊢ U (x) \neq Z (x) \leftrightarrow Z (x) \neq U (x)$
127	126	rabbii	$⊢ \{x \in On \| U (x) \neq Z (x)\} = \{x \in On \| Z (x) \neq U (x)\}$
128	127	inteqi	$⊢ ⋂ \{x \in On \| U (x) \neq Z (x)\} = ⋂ \{x \in On \| Z (x) \neq U (x)\}$
129	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$
130	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$
131	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$
132	131	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$
133		nosepssdm	$⊢ (Z \in No \land U \in No \land Z \neq U) \to ⋂ \{x \in On \| Z (x) \neq U (x)\} \subseteq dom Z$
134	129 130 132 133	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$
135	128 134	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$
136	125 135	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$
137		dfss2	$⊢ dom U \subseteq dom Z \leftrightarrow dom U \cap dom Z = dom U$
138	136 137	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$
139	124 138	eqtrid	$⊢ ((((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$
140	139	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)$
141		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$
142	141	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)$
143	130 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$
144		onelon	$⊢ (dom U \in On \land q \in dom U) \to q \in On$
145	143 144	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$
146	125	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)$
147	146	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)\}$
148	145 147 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)$
149		nesym	$⊢ U (q) \neq Z (q) \leftrightarrow \neg Z (q) = U (q)$
150	149	con2bii	$⊢ Z (q) = U (q) \leftrightarrow \neg U (q) \neq Z (q)$
151	148 150	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)$
152	142 151	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)$
153	152	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))$
154	140 153	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))$
155	154	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)$
156		nofun	$⊢ Z \in No \to Fun Z$
157		funres	$⊢ Fun Z \to Fun ({Z ↾}_{dom U})$
158	129 156 157	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})$
159	130 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$
160		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)))$
161	158 159 160	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)))$
162	139 155 161	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$
163	129 156	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$
164		funfn	$⊢ Fun Z \leftrightarrow Z Fn dom Z$
165	163 164	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$
166		1oex	$⊢ 1_{𝑜} \in V$
167	166	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
168	167	nosgnn0i	$⊢ \emptyset \neq 1_{𝑜}$
169		ndmfv	$⊢ \neg dom U \in dom U \to U (dom U) = \emptyset$
170	130 79 80 169	4syl	$⊢ ((((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$
171	170	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_{𝑜})$
172	168 171	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_{𝑜}$
173	172	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_{𝑜}$
174	173	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)$
175	173	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_{𝑜})$
176		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$
177	130 129 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)\}))$
178	176 177	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)\})$
179		fveq2	$⊢ ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U \to U (⋂ \{x \in On \| U (x) \neq Z (x)\}) = U (dom U)$
180	179	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)$
181		fveq2	$⊢ ⋂ \{x \in On \| U (x) \neq Z (x)\} = dom U \to Z (⋂ \{x \in On \| U (x) \neq Z (x)\}) = Z (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 Z (⋂ \{x \in On \| U (x) \neq Z (x)\}) = Z (dom U)$
183	178 180 182	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)$
184		fvex	$⊢ U (dom U) \in V$
185		fvex	$⊢ Z (dom U) \in V$
186	184 185	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_{𝑜}))$
187		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))$
188		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_{𝑜}))$
189	186 187 188	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_{𝑜}))$
190	183 189	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_{𝑜}))$
191	174 175 190	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_{𝑜})$
192	191	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_{𝑜}$
193		ndmfv	$⊢ \neg dom U \in dom Z \to Z (dom U) = \emptyset$
194	104	nosgnn0i	$⊢ \emptyset \neq 2_{𝑜}$
195		neeq1	$⊢ Z (dom U) = \emptyset \to (Z (dom U) \neq 2_{𝑜} \leftrightarrow \emptyset \neq 2_{𝑜})$
196	194 195	mpbiri	$⊢ Z (dom U) = \emptyset \to Z (dom U) \neq 2_{𝑜}$
197	196	neneqd	$⊢ Z (dom U) = \emptyset \to \neg Z (dom U) = 2_{𝑜}$
198	193 197	syl	$⊢ \neg dom U \in dom Z \to \neg Z (dom U) = 2_{𝑜}$
199	198	con4i	$⊢ Z (dom U) = 2_{𝑜} \to dom U \in dom Z$
200	192 199	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$
201		fnressn	$⊢ (Z Fn dom Z \land dom U \in dom Z) \to {Z ↾}_{\{dom U\}} = \{⟨dom U, Z (dom U)⟩\}$
202	165 200 201	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)⟩\}$
203	192	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_{𝑜}⟩$
204	203	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_{𝑜}⟩\}$
205	202 204	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_{𝑜}⟩\}$
206	162 205	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_{𝑜}⟩\}$
207	123 206	eqtrid	$⊢ ((((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_{𝑜}⟩\}$
208		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_{𝑜}⟩\})$
209	12 208	mpan	$⊢ U \cup \{⟨dom U, 2_{𝑜}⟩\} \in No \to \neg (U \cup \{⟨dom U, 2_{𝑜}⟩\}) <_{s} (U \cup \{⟨dom U, 2_{𝑜}⟩\})$
210	130 105 209	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_{𝑜}⟩\})$
211	207 210	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_{𝑜}⟩\})$
212	119 211	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_{𝑜}⟩\})$
213	212	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_{𝑜}⟩\}))$
214	29 213	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_{𝑜}⟩\}))$
215	23 214	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_{𝑜}⟩\})$
216	5 215	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