noetasuplem4

Description: Lemma for noeta . When A and B are separated, then Z is a lower bound for B . Part of Theorem 5.1 of Lipparini p. 7-8. (Contributed by Scott Fenton, 7-Dec-2021)

	Ref	Expression
Hypotheses	noetasuplem.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	noetasuplem.2	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
Assertion	noetasuplem4	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to \forall b \in B Z <_{s} b$

Proof

Step	Hyp	Ref	Expression
1		noetasuplem.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		noetasuplem.2	$⊢ Z = S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
3		ralcom	$⊢ \forall a \in A \forall b \in B a <_{s} b \leftrightarrow \forall b \in B \forall a \in A a <_{s} b$
4		simplll	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to A \subseteq No$
5		simpllr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to A \in V$
6		simprl	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to B \subseteq No$
7	6	sselda	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to b \in No$
8	1	nosupbnd2	$⊢ (A \subseteq No \land A \in V \land b \in No) \to (\forall a \in A a <_{s} b \leftrightarrow \neg ({b ↾}_{dom S}) <_{s} S)$
9	4 5 7 8	syl3anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to (\forall a \in A a <_{s} b \leftrightarrow \neg ({b ↾}_{dom S}) <_{s} S)$
10		simpl	$⊢ (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S) \to b \in B$
11		ssel2	$⊢ (B \subseteq No \land b \in B) \to b \in No$
12	6 10 11	syl2an	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to b \in No$
13		nodmord	$⊢ b \in No \to Ord dom b$
14		ordirr	$⊢ Ord dom b \to \neg dom b \in dom b$
15	12 13 14	3syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to \neg dom b \in dom b$
16		ssun2	$⊢ suc ⋃ bday [B] \subseteq dom S \cup suc ⋃ bday [B]$
17		bdayval	$⊢ b \in No \to bday (b) = dom b$
18	12 17	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to bday (b) = dom b$
19		bdayfo	$⊢ bday : No \underset{onto}{⟶} On$
20		fofn	$⊢ bday : No \underset{onto}{⟶} On \to bday Fn No$
21	19 20	ax-mp	$⊢ bday Fn No$
22		fnfvima	$⊢ (bday Fn No \land B \subseteq No \land b \in B) \to bday (b) \in bday [B]$
23	21 22	mp3an1	$⊢ (B \subseteq No \land b \in B) \to bday (b) \in bday [B]$
24	6 10 23	syl2an	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to bday (b) \in bday [B]$
25	18 24	eqeltrrd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to dom b \in bday [B]$
26		elssuni	$⊢ dom b \in bday [B] \to dom b \subseteq ⋃ bday [B]$
27	25 26	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to dom b \subseteq ⋃ bday [B]$
28		nodmon	$⊢ b \in No \to dom b \in On$
29		imassrn	$⊢ bday [B] \subseteq ran bday$
30		forn	$⊢ bday : No \underset{onto}{⟶} On \to ran bday = On$
31	19 30	ax-mp	$⊢ ran bday = On$
32	29 31	sseqtri	$⊢ bday [B] \subseteq On$
33		ssorduni	$⊢ bday [B] \subseteq On \to Ord ⋃ bday [B]$
34	32 33	ax-mp	$⊢ Ord ⋃ bday [B]$
35		ordsssuc	$⊢ (dom b \in On \land Ord ⋃ bday [B]) \to (dom b \subseteq ⋃ bday [B] \leftrightarrow dom b \in suc ⋃ bday [B])$
36	34 35	mpan2	$⊢ dom b \in On \to (dom b \subseteq ⋃ bday [B] \leftrightarrow dom b \in suc ⋃ bday [B])$
37	12 28 36	3syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to (dom b \subseteq ⋃ bday [B] \leftrightarrow dom b \in suc ⋃ bday [B])$
38	27 37	mpbid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to dom b \in suc ⋃ bday [B]$
39	16 38	sselid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to dom b \in (dom S \cup suc ⋃ bday [B])$
40		eleq2	$⊢ dom S \cup suc ⋃ bday [B] = dom b \to (dom b \in (dom S \cup suc ⋃ bday [B]) \leftrightarrow dom b \in dom b)$
41	39 40	syl5ibcom	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to (dom S \cup suc ⋃ bday [B] = dom b \to dom b \in dom b)$
42	15 41	mtod	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to \neg dom S \cup suc ⋃ bday [B] = dom b$
43	2	dmeqi	$⊢ dom Z = dom (S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}))$
44		dmun	$⊢ dom (S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) = dom S \cup dom ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
45	43 44	eqtri	$⊢ dom Z = dom S \cup dom ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})$
46		1oex	$⊢ 1_{𝑜} \in V$
47	46	snnz	$⊢ \{1_{𝑜}\} \neq \emptyset$
48		dmxp	$⊢ \{1_{𝑜}\} \neq \emptyset \to dom ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) = suc ⋃ bday [B] ∖ dom S$
49	47 48	ax-mp	$⊢ dom ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) = suc ⋃ bday [B] ∖ dom S$
50	49	uneq2i	$⊢ dom S \cup dom ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) = dom S \cup (suc ⋃ bday [B] ∖ dom S)$
51		undif2	$⊢ dom S \cup (suc ⋃ bday [B] ∖ dom S) = dom S \cup suc ⋃ bday [B]$
52	45 50 51	3eqtri	$⊢ dom Z = dom S \cup suc ⋃ bday [B]$
53		dmeq	$⊢ Z = b \to dom Z = dom b$
54	52 53	eqtr3id	$⊢ Z = b \to dom S \cup suc ⋃ bday [B] = dom b$
55	42 54	nsyl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to \neg Z = b$
56		df-ne	$⊢ Z \neq b \leftrightarrow \neg Z = b$
57		notnotr	$⊢ \neg \neg dom ({b ↾}_{dom S}) = dom S \to dom ({b ↾}_{dom S}) = dom S$
58		simpr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S$
59	58	fvresd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ({Z ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\}) = Z (⋂ \{p \in On \| Z (p) \neq b (p)\})$
60	2	reseq1i	$⊢ {Z ↾}_{dom S} = {(S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) ↾}_{dom S}$
61		resundir	$⊢ {(S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) ↾}_{dom S} = ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S})$
62		df-res	$⊢ {((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S} = ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V)$
63		disjdifr	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset$
64		xpdisj1	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
65	63 64	ax-mp	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
66	62 65	eqtri	$⊢ {((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S} = \emptyset$
67	66	uneq2i	$⊢ ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S}) = ({S ↾}_{dom S}) \cup \emptyset$
68		un0	$⊢ ({S ↾}_{dom S}) \cup \emptyset = {S ↾}_{dom S}$
69	67 68	eqtri	$⊢ ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S}) = {S ↾}_{dom S}$
70	60 61 69	3eqtri	$⊢ {Z ↾}_{dom S} = {S ↾}_{dom S}$
71		simplll	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to (A \subseteq No \land A \in V)$
72	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
73	71 72	syl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to S \in No$
74	73	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to S \in No$
75		nofun	$⊢ S \in No \to Fun S$
76	74 75	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to Fun S$
77		funrel	$⊢ Fun S \to Rel S$
78		resdm	$⊢ Rel S \to {S ↾}_{dom S} = S$
79	76 77 78	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to {S ↾}_{dom S} = S$
80	70 79	syl5eq	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to {Z ↾}_{dom S} = S$
81	80	fveq1d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ({Z ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\}) = S (⋂ \{p \in On \| Z (p) \neq b (p)\})$
82	59 81	eqtr3d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to Z (⋂ \{p \in On \| Z (p) \neq b (p)\}) = S (⋂ \{p \in On \| Z (p) \neq b (p)\})$
83		simp-4l	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to A \subseteq No$
84		simp-4r	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to A \in V$
85		simplrr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to B \in V$
86	85	adantr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to B \in V$
87	1 2	noetasuplem1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to Z \in No$
88	83 84 86 87	syl3anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to Z \in No$
89	88	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to Z \in No$
90	12	adantr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to b \in No$
91	90	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to b \in No$
92		simplr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to Z \neq b$
93		nosepne	$⊢ (Z \in No \land b \in No \land Z \neq b) \to Z (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq b (⋂ \{p \in On \| Z (p) \neq b (p)\})$
94	89 91 92 93	syl3anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to Z (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq b (⋂ \{p \in On \| Z (p) \neq b (p)\})$
95	82 94	eqnetrrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to S (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq b (⋂ \{p \in On \| Z (p) \neq b (p)\})$
96	58	fvresd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\}) = b (⋂ \{p \in On \| Z (p) \neq b (p)\})$
97	95 96	neeqtrrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to S (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\})$
98		fveq2	$⊢ q = ⋂ \{p \in On \| Z (p) \neq b (p)\} \to ({b ↾}_{dom S}) (q) = ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\})$
99		fveq2	$⊢ q = ⋂ \{p \in On \| Z (p) \neq b (p)\} \to S (q) = S (⋂ \{p \in On \| Z (p) \neq b (p)\})$
100	98 99	neeq12d	$⊢ q = ⋂ \{p \in On \| Z (p) \neq b (p)\} \to (({b ↾}_{dom S}) (q) \neq S (q) \leftrightarrow ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq S (⋂ \{p \in On \| Z (p) \neq b (p)\}))$
101		df-ne	$⊢ ({b ↾}_{dom S}) (q) \neq S (q) \leftrightarrow \neg ({b ↾}_{dom S}) (q) = S (q)$
102		necom	$⊢ ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq S (⋂ \{p \in On \| Z (p) \neq b (p)\}) \leftrightarrow S (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\})$
103	100 101 102	3bitr3g	$⊢ q = ⋂ \{p \in On \| Z (p) \neq b (p)\} \to (\neg ({b ↾}_{dom S}) (q) = S (q) \leftrightarrow S (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\}))$
104	103	rspcev	$⊢ (⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S \land S (⋂ \{p \in On \| Z (p) \neq b (p)\}) \neq ({b ↾}_{dom S}) (⋂ \{p \in On \| Z (p) \neq b (p)\})) \to \exists q \in dom S \neg ({b ↾}_{dom S}) (q) = S (q)$
105	58 97 104	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to \exists q \in dom S \neg ({b ↾}_{dom S}) (q) = S (q)$
106		rexeq	$⊢ dom ({b ↾}_{dom S}) = dom S \to (\exists q \in dom ({b ↾}_{dom S}) \neg ({b ↾}_{dom S}) (q) = S (q) \leftrightarrow \exists q \in dom S \neg ({b ↾}_{dom S}) (q) = S (q))$
107	105 106	syl5ibrcom	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (dom ({b ↾}_{dom S}) = dom S \to \exists q \in dom ({b ↾}_{dom S}) \neg ({b ↾}_{dom S}) (q) = S (q))$
108		rexnal	$⊢ \exists q \in dom ({b ↾}_{dom S}) \neg ({b ↾}_{dom S}) (q) = S (q) \leftrightarrow \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q)$
109	107 108	syl6ib	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (dom ({b ↾}_{dom S}) = dom S \to \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q))$
110	57 109	syl5	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (\neg \neg dom ({b ↾}_{dom S}) = dom S \to \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q))$
111	110	orrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (\neg dom ({b ↾}_{dom S}) = dom S \lor \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q))$
112		nofun	$⊢ b \in No \to Fun b$
113		funres	$⊢ Fun b \to Fun ({b ↾}_{dom S})$
114	91 112 113	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to Fun ({b ↾}_{dom S})$
115		eqfunfv	$⊢ (Fun ({b ↾}_{dom S}) \land Fun S) \to ({b ↾}_{dom S} = S \leftrightarrow (dom ({b ↾}_{dom S}) = dom S \land \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q)))$
116	114 76 115	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ({b ↾}_{dom S} = S \leftrightarrow (dom ({b ↾}_{dom S}) = dom S \land \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q)))$
117		ianor	$⊢ \neg (dom ({b ↾}_{dom S}) = dom S \land \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q)) \leftrightarrow (\neg dom ({b ↾}_{dom S}) = dom S \lor \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q))$
118	117	con1bii	$⊢ \neg (\neg dom ({b ↾}_{dom S}) = dom S \lor \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q)) \leftrightarrow (dom ({b ↾}_{dom S}) = dom S \land \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q))$
119	116 118	bitr4di	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ({b ↾}_{dom S} = S \leftrightarrow \neg (\neg dom ({b ↾}_{dom S}) = dom S \lor \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q)))$
120	119	con2bid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ((\neg dom ({b ↾}_{dom S}) = dom S \lor \neg \forall q \in dom ({b ↾}_{dom S}) ({b ↾}_{dom S}) (q) = S (q)) \leftrightarrow \neg {b ↾}_{dom S} = S)$
121	111 120	mpbid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to \neg {b ↾}_{dom S} = S$
122	121	pm2.21d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ({b ↾}_{dom S} = S \to Z <_{s} b)$
123	80	breq1d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (({Z ↾}_{dom S}) <_{s} ({b ↾}_{dom S}) \leftrightarrow S <_{s} ({b ↾}_{dom S}))$
124		nodmon	$⊢ S \in No \to dom S \in On$
125	74 124	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to dom S \in On$
126		sltres	$⊢ (Z \in No \land b \in No \land dom S \in On) \to (({Z ↾}_{dom S}) <_{s} ({b ↾}_{dom S}) \to Z <_{s} b)$
127	89 91 125 126	syl3anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (({Z ↾}_{dom S}) <_{s} ({b ↾}_{dom S}) \to Z <_{s} b)$
128	123 127	sylbird	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (S <_{s} ({b ↾}_{dom S}) \to Z <_{s} b)$
129		simplrr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to \neg ({b ↾}_{dom S}) <_{s} S$
130	129	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to \neg ({b ↾}_{dom S}) <_{s} S$
131		noreson	$⊢ (b \in No \land dom S \in On) \to {b ↾}_{dom S} \in No$
132	91 125 131	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to {b ↾}_{dom S} \in No$
133		sltso	$⊢ <_{s} Or No$
134		sotric	$⊢ (<_{s} Or No \land ({b ↾}_{dom S} \in No \land S \in No)) \to (({b ↾}_{dom S}) <_{s} S \leftrightarrow \neg ({b ↾}_{dom S} = S \lor S <_{s} ({b ↾}_{dom S})))$
135	133 134	mpan	$⊢ ({b ↾}_{dom S} \in No \land S \in No) \to (({b ↾}_{dom S}) <_{s} S \leftrightarrow \neg ({b ↾}_{dom S} = S \lor S <_{s} ({b ↾}_{dom S})))$
136	132 74 135	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (({b ↾}_{dom S}) <_{s} S \leftrightarrow \neg ({b ↾}_{dom S} = S \lor S <_{s} ({b ↾}_{dom S})))$
137	136	con2bid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to (({b ↾}_{dom S} = S \lor S <_{s} ({b ↾}_{dom S})) \leftrightarrow \neg ({b ↾}_{dom S}) <_{s} S)$
138	130 137	mpbird	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to ({b ↾}_{dom S} = S \lor S <_{s} ({b ↾}_{dom S}))$
139	122 128 138	mpjaod	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S) \to Z <_{s} b$
140	88	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to Z \in No$
141	90	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to b \in No$
142		simplr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to Z \neq b$
143	2	fveq1i	$⊢ Z (⋂ \{p \in On \| Z (p) \neq b (p)\}) = (S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) (⋂ \{p \in On \| Z (p) \neq b (p)\})$
144		simp-4l	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to (A \subseteq No \land A \in V)$
145	144 72 75	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to Fun S$
146		funfn	$⊢ Fun S \leftrightarrow S Fn dom S$
147	145 146	sylib	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to S Fn dom S$
148	46	fconst	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) : suc ⋃ bday [B] ∖ dom S ⟶ \{1_{𝑜}\}$
149		ffn	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) : suc ⋃ bday [B] ∖ dom S ⟶ \{1_{𝑜}\} \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) Fn (suc ⋃ bday [B] ∖ dom S)$
150	148 149	ax-mp	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) Fn (suc ⋃ bday [B] ∖ dom S)$
151	150	a1i	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) Fn (suc ⋃ bday [B] ∖ dom S)$
152		disjdif	$⊢ dom S \cap (suc ⋃ bday [B] ∖ dom S) = \emptyset$
153	152	a1i	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to dom S \cap (suc ⋃ bday [B] ∖ dom S) = \emptyset$
154		necom	$⊢ Z (p) \neq b (p) \leftrightarrow b (p) \neq Z (p)$
155	154	rabbii	$⊢ \{p \in On \| Z (p) \neq b (p)\} = \{p \in On \| b (p) \neq Z (p)\}$
156	155	inteqi	$⊢ ⋂ \{p \in On \| Z (p) \neq b (p)\} = ⋂ \{p \in On \| b (p) \neq Z (p)\}$
157	142	necomd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to b \neq Z$
158		nosepssdm	$⊢ (b \in No \land Z \in No \land b \neq Z) \to ⋂ \{p \in On \| b (p) \neq Z (p)\} \subseteq dom b$
159	141 140 157 158	syl3anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ⋂ \{p \in On \| b (p) \neq Z (p)\} \subseteq dom b$
160	156 159	eqsstrid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \subseteq dom b$
161	141 17	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to bday (b) = dom b$
162		simplrl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to B \subseteq No$
163	162	adantr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to B \subseteq No$
164	163	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to B \subseteq No$
165		simplrl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to b \in B$
166	165	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to b \in B$
167	164 166 23	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to bday (b) \in bday [B]$
168	161 167	eqeltrrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to dom b \in bday [B]$
169	168 26	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to dom b \subseteq ⋃ bday [B]$
170	141 28 36	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to (dom b \subseteq ⋃ bday [B] \leftrightarrow dom b \in suc ⋃ bday [B])$
171	169 170	mpbid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to dom b \in suc ⋃ bday [B]$
172		nosepon	$⊢ (Z \in No \land b \in No \land Z \neq b) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in On$
173	140 141 142 172	syl3anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in On$
174		eloni	$⊢ ⋂ \{p \in On \| Z (p) \neq b (p)\} \in On \to Ord ⋂ \{p \in On \| Z (p) \neq b (p)\}$
175		ordsuc	$⊢ Ord ⋃ bday [B] \leftrightarrow Ord suc ⋃ bday [B]$
176	34 175	mpbi	$⊢ Ord suc ⋃ bday [B]$
177		ordtr2	$⊢ (Ord ⋂ \{p \in On \| Z (p) \neq b (p)\} \land Ord suc ⋃ bday [B]) \to ((⋂ \{p \in On \| Z (p) \neq b (p)\} \subseteq dom b \land dom b \in suc ⋃ bday [B]) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in suc ⋃ bday [B])$
178	176 177	mpan2	$⊢ Ord ⋂ \{p \in On \| Z (p) \neq b (p)\} \to ((⋂ \{p \in On \| Z (p) \neq b (p)\} \subseteq dom b \land dom b \in suc ⋃ bday [B]) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in suc ⋃ bday [B])$
179	173 174 178	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ((⋂ \{p \in On \| Z (p) \neq b (p)\} \subseteq dom b \land dom b \in suc ⋃ bday [B]) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in suc ⋃ bday [B])$
180	160 171 179	mp2and	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in suc ⋃ bday [B]$
181		simpr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}$
182	144 72 124	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to dom S \in On$
183		ontri1	$⊢ (dom S \in On \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in On) \to (dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\} \leftrightarrow \neg ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S)$
184	182 173 183	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to (dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\} \leftrightarrow \neg ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S)$
185	181 184	mpbid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to \neg ⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S$
186	180 185	eldifd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in (suc ⋃ bday [B] ∖ dom S)$
187		fvun2	$⊢ (S Fn dom S \land ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) Fn (suc ⋃ bday [B] ∖ dom S) \land (dom S \cap (suc ⋃ bday [B] ∖ dom S) = \emptyset \land ⋂ \{p \in On \| Z (p) \neq b (p)\} \in (suc ⋃ bday [B] ∖ dom S))) \to (S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) (⋂ \{p \in On \| Z (p) \neq b (p)\}) = ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) (⋂ \{p \in On \| Z (p) \neq b (p)\})$
188	147 151 153 186 187	syl112anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to (S \cup ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\})) (⋂ \{p \in On \| Z (p) \neq b (p)\}) = ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) (⋂ \{p \in On \| Z (p) \neq b (p)\})$
189	143 188	syl5eq	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to Z (⋂ \{p \in On \| Z (p) \neq b (p)\}) = ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) (⋂ \{p \in On \| Z (p) \neq b (p)\})$
190	46	fvconst2	$⊢ ⋂ \{p \in On \| Z (p) \neq b (p)\} \in (suc ⋃ bday [B] ∖ dom S) \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) (⋂ \{p \in On \| Z (p) \neq b (p)\}) = 1_{𝑜}$
191	186 190	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) (⋂ \{p \in On \| Z (p) \neq b (p)\}) = 1_{𝑜}$
192	189 191	eqtrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to Z (⋂ \{p \in On \| Z (p) \neq b (p)\}) = 1_{𝑜}$
193		nosep1o	$⊢ ((Z \in No \land b \in No \land Z \neq b) \land Z (⋂ \{p \in On \| Z (p) \neq b (p)\}) = 1_{𝑜}) \to Z <_{s} b$
194	140 141 142 192 193	syl31anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \land dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\}) \to Z <_{s} b$
195		simpr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to Z \neq b$
196	88 90 195 172	syl3anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in On$
197	196 174	syl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to Ord ⋂ \{p \in On \| Z (p) \neq b (p)\}$
198		nodmord	$⊢ S \in No \to Ord dom S$
199	71 72 198	3syl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to Ord dom S$
200		ordtri2or	$⊢ (Ord ⋂ \{p \in On \| Z (p) \neq b (p)\} \land Ord dom S) \to (⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S \lor dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\})$
201	197 199 200	syl2anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to (⋂ \{p \in On \| Z (p) \neq b (p)\} \in dom S \lor dom S \subseteq ⋂ \{p \in On \| Z (p) \neq b (p)\})$
202	139 194 201	mpjaodan	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \land Z \neq b) \to Z <_{s} b$
203	202	ex	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to (Z \neq b \to Z <_{s} b)$
204	56 203	syl5bir	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to (\neg Z = b \to Z <_{s} b)$
205	55 204	mpd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (b \in B \land \neg ({b ↾}_{dom S}) <_{s} S)) \to Z <_{s} b$
206	205	expr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to (\neg ({b ↾}_{dom S}) <_{s} S \to Z <_{s} b)$
207	9 206	sylbid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land b \in B) \to (\forall a \in A a <_{s} b \to Z <_{s} b)$
208	207	ralimdva	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to (\forall b \in B \forall a \in A a <_{s} b \to \forall b \in B Z <_{s} b)$
209	3 208	syl5bi	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to (\forall a \in A \forall b \in B a <_{s} b \to \forall b \in B Z <_{s} b)$
210	209	3impia	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land \forall a \in A \forall b \in B a <_{s} b) \to \forall b \in B Z <_{s} b$

Metamath Proof Explorer

Theorem noetasuplem4

Proof