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	sseldi	$⊢ (((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		incom	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = dom S \cap (suc ⋃ bday [B] ∖ dom S)$
64		disjdif	$⊢ dom S \cap (suc ⋃ bday [B] ∖ dom S) = \emptyset$
65	63 64	eqtri	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset$
66		xpdisj1	$⊢ (suc ⋃ bday [B] ∖ dom S) \cap dom S = \emptyset \to ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
67	65 66	ax-mp	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) \cap (dom S \times V) = \emptyset$
68	62 67	eqtri	$⊢ {((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S} = \emptyset$
69	68	uneq2i	$⊢ ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S}) = ({S ↾}_{dom S}) \cup \emptyset$
70		un0	$⊢ ({S ↾}_{dom S}) \cup \emptyset = {S ↾}_{dom S}$
71	69 70	eqtri	$⊢ ({S ↾}_{dom S}) \cup ({((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) ↾}_{dom S}) = {S ↾}_{dom S}$
72	60 61 71	3eqtri	$⊢ {Z ↾}_{dom S} = {S ↾}_{dom S}$
73		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)$
74	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
75	73 74	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$
76	75	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$
77		nofun	$⊢ S \in No \to Fun S$
78	76 77	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$
79		funrel	$⊢ Fun S \to Rel S$
80		resdm	$⊢ Rel S \to {S ↾}_{dom S} = S$
81	78 79 80	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$
82	72 81	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$
83	82	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)\})$
84	59 83	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)\})$
85		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$
86		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$
87		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$
88	87	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$
89	1 2	noetasuplem1	$⊢ (A \subseteq No \land A \in V \land B \in V) \to Z \in No$
90	85 86 88 89	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$
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 Z \in No$
92	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$
93	92	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$
94		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$
95		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)\})$
96	91 93 94 95	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)\})$
97	84 96	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)\})$
98	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)\})$
99	97 98	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)\})$
100		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)\})$
101		fveq2	$⊢ q = ⋂ \{p \in On \| Z (p) \neq b (p)\} \to S (q) = S (⋂ \{p \in On \| Z (p) \neq b (p)\})$
102	100 101	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)\}))$
103		df-ne	$⊢ ({b ↾}_{dom S}) (q) \neq S (q) \leftrightarrow \neg ({b ↾}_{dom S}) (q) = S (q)$
104		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)\})$
105	102 103 104	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)\}))$
106	105	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)$
107	58 99 106	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)$
108		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))$
109	107 108	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))$
110		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)$
111	109 110	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))$
112	57 111	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))$
113	112	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))$
114		nofun	$⊢ b \in No \to Fun b$
115		funres	$⊢ Fun b \to Fun ({b ↾}_{dom S})$
116	93 114 115	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})$
117		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)))$
118	116 78 117	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)))$
119		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))$
120	119	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))$
121	118 120	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)))$
122	121	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)$
123	113 122	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$
124	123	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)$
125	82	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}))$
126		nodmon	$⊢ S \in No \to dom S \in On$
127	76 126	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$
128		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)$
129	91 93 127 128	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)$
130	125 129	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)$
131		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$
132	131	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$
133		noreson	$⊢ (b \in No \land dom S \in On) \to {b ↾}_{dom S} \in No$
134	93 127 133	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$
135		sltso	$⊢ <_{s} Or No$
136		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})))$
137	135 136	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})))$
138	134 76 137	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})))$
139	138	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)$
140	132 139	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}))$
141	124 130 140	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$
142	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 Z \in No$
143	92	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$
144		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$
145	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)\})$
146		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)$
147	146 74 77	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$
148		funfn	$⊢ Fun S \leftrightarrow S Fn dom S$
149	147 148	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$
150	46	fconst	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) : suc ⋃ bday [B] ∖ dom S ⟶ \{1_{𝑜}\}$
151		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)$
152	150 151	ax-mp	$⊢ ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) Fn (suc ⋃ bday [B] ∖ dom S)$
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 ((suc ⋃ bday [B] ∖ dom S) \times \{1_{𝑜}\}) Fn (suc ⋃ bday [B] ∖ dom S)$
154	64	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$
155		necom	$⊢ Z (p) \neq b (p) \leftrightarrow b (p) \neq Z (p)$
156	155	rabbii	$⊢ \{p \in On \| Z (p) \neq b (p)\} = \{p \in On \| b (p) \neq Z (p)\}$
157	156	inteqi	$⊢ ⋂ \{p \in On \| Z (p) \neq b (p)\} = ⋂ \{p \in On \| b (p) \neq Z (p)\}$
158	144	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$
159		nosepssdm	$⊢ (b \in No \land Z \in No \land b \neq Z) \to ⋂ \{p \in On \| b (p) \neq Z (p)\} \subseteq dom b$
160	143 142 158 159	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$
161	157 160	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$
162	143 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$
163		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$
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) \to B \subseteq No$
165	164	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$
166		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$
167	166	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$
168	165 167 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]$
169	162 168	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]$
170	169 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]$
171	143 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])$
172	170 171	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]$
173		nosepon	$⊢ (Z \in No \land b \in No \land Z \neq b) \to ⋂ \{p \in On \| Z (p) \neq b (p)\} \in On$
174	142 143 144 173	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$
175		eloni	$⊢ ⋂ \{p \in On \| Z (p) \neq b (p)\} \in On \to Ord ⋂ \{p \in On \| Z (p) \neq b (p)\}$
176		ordsuc	$⊢ Ord ⋃ bday [B] \leftrightarrow Ord suc ⋃ bday [B]$
177	34 176	mpbi	$⊢ Ord suc ⋃ bday [B]$
178		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])$
179	177 178	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])$
180	174 175 179	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])$
181	161 172 180	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]$
182		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)\}$
183	146 74 126	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$
184		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)$
185	183 174 184	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)$
186	182 185	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$
187	181 186	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)$
188		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)\})$
189	149 153 154 187 188	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)\})$
190	145 189	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)\})$
191	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_{𝑜}$
192	187 191	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_{𝑜}$
193	190 192	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_{𝑜}$
194		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$
195	142 143 144 193 194	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$
196		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$
197	90 92 196 173	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$
198	197 175	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)\}$
199		nodmord	$⊢ S \in No \to Ord dom S$
200	73 74 199	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$
201		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)\})$
202	198 200 201	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)\})$
203	141 195 202	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$
204	203	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)$
205	56 204	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)$
206	55 205	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$
207	206	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)$
208	9 207	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)$
209	208	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)$
210	3 209	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)$
211	210	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