noetainflem4

Description: Lemma for noeta . If A precedes B , then W is greater than A . (Contributed by Scott Fenton, 9-Aug-2024)

	Ref	Expression
Hypotheses	noetainflem.1	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	noetainflem.2	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
Assertion	noetainflem4	$⊢ ((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 a \in A a <_{s} W$

Proof

Step	Hyp	Ref	Expression
1		noetainflem.1	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		noetainflem.2	$⊢ W = T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
3		simplrl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to B \subseteq No$
4		simplrr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to B \in V$
5		simpll	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \to A \subseteq No$
6	5	sselda	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to a \in No$
7	1	noinfbnd2	$⊢ (B \subseteq No \land B \in V \land a \in No) \to (\forall b \in B a <_{s} b \leftrightarrow \neg T <_{s} ({a ↾}_{dom T}))$
8	3 4 6 7	syl3anc	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to (\forall b \in B a <_{s} b \leftrightarrow \neg T <_{s} ({a ↾}_{dom T}))$
9		simplll	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to A \subseteq No$
10		simprl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to a \in A$
11	9 10	sseldd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to a \in No$
12		nodmord	$⊢ a \in No \to Ord dom a$
13		ordirr	$⊢ Ord dom a \to \neg dom a \in dom a$
14	11 12 13	3syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to \neg dom a \in dom a$
15		bdayval	$⊢ a \in No \to bday (a) = dom a$
16	11 15	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to bday (a) = dom a$
17		bdayfo	$⊢ bday : No \underset{onto}{⟶} On$
18		fofn	$⊢ bday : No \underset{onto}{⟶} On \to bday Fn No$
19	17 18	ax-mp	$⊢ bday Fn No$
20		fnfvima	$⊢ (bday Fn No \land A \subseteq No \land a \in A) \to bday (a) \in bday [A]$
21	19 9 10 20	mp3an2i	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to bday (a) \in bday [A]$
22	16 21	eqeltrrd	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to dom a \in bday [A]$
23		elssuni	$⊢ dom a \in bday [A] \to dom a \subseteq ⋃ bday [A]$
24	22 23	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to dom a \subseteq ⋃ bday [A]$
25		nodmon	$⊢ a \in No \to dom a \in On$
26		imassrn	$⊢ bday [A] \subseteq ran bday$
27		forn	$⊢ bday : No \underset{onto}{⟶} On \to ran bday = On$
28	17 27	ax-mp	$⊢ ran bday = On$
29	26 28	sseqtri	$⊢ bday [A] \subseteq On$
30		ssorduni	$⊢ bday [A] \subseteq On \to Ord ⋃ bday [A]$
31	29 30	ax-mp	$⊢ Ord ⋃ bday [A]$
32		ordsssuc	$⊢ (dom a \in On \land Ord ⋃ bday [A]) \to (dom a \subseteq ⋃ bday [A] \leftrightarrow dom a \in suc ⋃ bday [A])$
33	31 32	mpan2	$⊢ dom a \in On \to (dom a \subseteq ⋃ bday [A] \leftrightarrow dom a \in suc ⋃ bday [A])$
34	11 25 33	3syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to (dom a \subseteq ⋃ bday [A] \leftrightarrow dom a \in suc ⋃ bday [A])$
35	24 34	mpbid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to dom a \in suc ⋃ bday [A]$
36		elun2	$⊢ dom a \in suc ⋃ bday [A] \to dom a \in (dom T \cup suc ⋃ bday [A])$
37	35 36	syl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to dom a \in (dom T \cup suc ⋃ bday [A])$
38		eleq2	$⊢ dom a = dom T \cup suc ⋃ bday [A] \to (dom a \in dom a \leftrightarrow dom a \in (dom T \cup suc ⋃ bday [A]))$
39	37 38	syl5ibrcom	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to (dom a = dom T \cup suc ⋃ bday [A] \to dom a \in dom a)$
40	14 39	mtod	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to \neg dom a = dom T \cup suc ⋃ bday [A]$
41		dmeq	$⊢ a = W \to dom a = dom W$
42	2	dmeqi	$⊢ dom W = dom (T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}))$
43		dmun	$⊢ dom (T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})) = dom T \cup dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})$
44		2oex	$⊢ 2_{𝑜} \in V$
45	44	snnz	$⊢ \{2_{𝑜}\} \neq \emptyset$
46		dmxp	$⊢ \{2_{𝑜}\} \neq \emptyset \to dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = suc ⋃ bday [A] ∖ dom T$
47	45 46	ax-mp	$⊢ dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = suc ⋃ bday [A] ∖ dom T$
48	47	uneq2i	$⊢ dom T \cup dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = dom T \cup (suc ⋃ bday [A] ∖ dom T)$
49		undif2	$⊢ dom T \cup (suc ⋃ bday [A] ∖ dom T) = dom T \cup suc ⋃ bday [A]$
50	48 49	eqtri	$⊢ dom T \cup dom ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) = dom T \cup suc ⋃ bday [A]$
51	42 43 50	3eqtri	$⊢ dom W = dom T \cup suc ⋃ bday [A]$
52	41 51	eqtrdi	$⊢ a = W \to dom a = dom T \cup suc ⋃ bday [A]$
53	40 52	nsyl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to \neg a = W$
54	53	neqned	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to a \neq W$
55		simpr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T$
56	11	adantr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to a \in No$
57	56	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to a \in No$
58		simp-4r	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to A \in V$
59		simplrl	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to B \subseteq No$
60	59	adantr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to B \subseteq No$
61		simplrr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to B \in V$
62	61	adantr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to B \in V$
63	1 2	noetainflem1	$⊢ (A \in V \land B \subseteq No \land B \in V) \to W \in No$
64	58 60 62 63	syl3anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to W \in No$
65	64	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to W \in No$
66		simplr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to a \neq W$
67		nosepne	$⊢ (a \in No \land W \in No \land a \neq W) \to a (⋂ \{p \in On \| a (p) \neq W (p)\}) \neq W (⋂ \{p \in On \| a (p) \neq W (p)\})$
68	57 65 66 67	syl3anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to a (⋂ \{p \in On \| a (p) \neq W (p)\}) \neq W (⋂ \{p \in On \| a (p) \neq W (p)\})$
69	55	fvresd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to ({W ↾}_{dom T}) (⋂ \{p \in On \| a (p) \neq W (p)\}) = W (⋂ \{p \in On \| a (p) \neq W (p)\})$
70		simp-4r	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (B \subseteq No \land B \in V)$
71	1 2	noetainflem2	$⊢ (B \subseteq No \land B \in V) \to {W ↾}_{dom T} = T$
72	70 71	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to {W ↾}_{dom T} = T$
73	72	fveq1d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to ({W ↾}_{dom T}) (⋂ \{p \in On \| a (p) \neq W (p)\}) = T (⋂ \{p \in On \| a (p) \neq W (p)\})$
74	69 73	eqtr3d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to W (⋂ \{p \in On \| a (p) \neq W (p)\}) = T (⋂ \{p \in On \| a (p) \neq W (p)\})$
75	68 74	neeqtrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to a (⋂ \{p \in On \| a (p) \neq W (p)\}) \neq T (⋂ \{p \in On \| a (p) \neq W (p)\})$
76	75	necomd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to T (⋂ \{p \in On \| a (p) \neq W (p)\}) \neq a (⋂ \{p \in On \| a (p) \neq W (p)\})$
77		fveq2	$⊢ q = ⋂ \{p \in On \| a (p) \neq W (p)\} \to T (q) = T (⋂ \{p \in On \| a (p) \neq W (p)\})$
78		fveq2	$⊢ q = ⋂ \{p \in On \| a (p) \neq W (p)\} \to a (q) = a (⋂ \{p \in On \| a (p) \neq W (p)\})$
79	77 78	neeq12d	$⊢ q = ⋂ \{p \in On \| a (p) \neq W (p)\} \to (T (q) \neq a (q) \leftrightarrow T (⋂ \{p \in On \| a (p) \neq W (p)\}) \neq a (⋂ \{p \in On \| a (p) \neq W (p)\}))$
80	79	rspcev	$⊢ (⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T \land T (⋂ \{p \in On \| a (p) \neq W (p)\}) \neq a (⋂ \{p \in On \| a (p) \neq W (p)\})) \to \exists q \in dom T T (q) \neq a (q)$
81	55 76 80	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to \exists q \in dom T T (q) \neq a (q)$
82		df-ne	$⊢ T (q) \neq ({a ↾}_{dom T}) (q) \leftrightarrow \neg T (q) = ({a ↾}_{dom T}) (q)$
83		fvres	$⊢ q \in dom T \to ({a ↾}_{dom T}) (q) = a (q)$
84	83	neeq2d	$⊢ q \in dom T \to (T (q) \neq ({a ↾}_{dom T}) (q) \leftrightarrow T (q) \neq a (q))$
85	82 84	bitr3id	$⊢ q \in dom T \to (\neg T (q) = ({a ↾}_{dom T}) (q) \leftrightarrow T (q) \neq a (q))$
86	85	rexbiia	$⊢ \exists q \in dom T \neg T (q) = ({a ↾}_{dom T}) (q) \leftrightarrow \exists q \in dom T T (q) \neq a (q)$
87		rexnal	$⊢ \exists q \in dom T \neg T (q) = ({a ↾}_{dom T}) (q) \leftrightarrow \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)$
88	86 87	bitr3i	$⊢ \exists q \in dom T T (q) \neq a (q) \leftrightarrow \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)$
89	81 88	sylib	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)$
90	89	olcd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (\neg dom T = dom ({a ↾}_{dom T}) \lor \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q))$
91	1	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
92	91	ad3antlr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to T \in No$
93	92	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to T \in No$
94		nofun	$⊢ T \in No \to Fun T$
95	93 94	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to Fun T$
96		nofun	$⊢ a \in No \to Fun a$
97		funres	$⊢ Fun a \to Fun ({a ↾}_{dom T})$
98	57 96 97	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to Fun ({a ↾}_{dom T})$
99		eqfunfv	$⊢ (Fun T \land Fun ({a ↾}_{dom T})) \to (T = {a ↾}_{dom T} \leftrightarrow (dom T = dom ({a ↾}_{dom T}) \land \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)))$
100	95 98 99	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (T = {a ↾}_{dom T} \leftrightarrow (dom T = dom ({a ↾}_{dom T}) \land \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)))$
101		ianor	$⊢ \neg (dom T = dom ({a ↾}_{dom T}) \land \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)) \leftrightarrow (\neg dom T = dom ({a ↾}_{dom T}) \lor \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q))$
102	101	con1bii	$⊢ \neg (\neg dom T = dom ({a ↾}_{dom T}) \lor \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)) \leftrightarrow (dom T = dom ({a ↾}_{dom T}) \land \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q))$
103	100 102	bitr4di	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (T = {a ↾}_{dom T} \leftrightarrow \neg (\neg dom T = dom ({a ↾}_{dom T}) \lor \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)))$
104	103	con2bid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to ((\neg dom T = dom ({a ↾}_{dom T}) \lor \neg \forall q \in dom T T (q) = ({a ↾}_{dom T}) (q)) \leftrightarrow \neg T = {a ↾}_{dom T})$
105	90 104	mpbid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to \neg T = {a ↾}_{dom T}$
106	105	pm2.21d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (T = {a ↾}_{dom T} \to a <_{s} W)$
107	72	breq2d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (({a ↾}_{dom T}) <_{s} ({W ↾}_{dom T}) \leftrightarrow ({a ↾}_{dom T}) <_{s} T)$
108		nodmon	$⊢ T \in No \to dom T \in On$
109	92 108	syl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to dom T \in On$
110	109	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to dom T \in On$
111		sltres	$⊢ (a \in No \land W \in No \land dom T \in On) \to (({a ↾}_{dom T}) <_{s} ({W ↾}_{dom T}) \to a <_{s} W)$
112	57 65 110 111	syl3anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (({a ↾}_{dom T}) <_{s} ({W ↾}_{dom T}) \to a <_{s} W)$
113	107 112	sylbird	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (({a ↾}_{dom T}) <_{s} T \to a <_{s} W)$
114		simplrr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to \neg T <_{s} ({a ↾}_{dom T})$
115	114	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to \neg T <_{s} ({a ↾}_{dom T})$
116		noreson	$⊢ (a \in No \land dom T \in On) \to {a ↾}_{dom T} \in No$
117	56 109 116	syl2anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to {a ↾}_{dom T} \in No$
118	117	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to {a ↾}_{dom T} \in No$
119		sltso	$⊢ <_{s} Or No$
120		sotric	$⊢ (<_{s} Or No \land (T \in No \land {a ↾}_{dom T} \in No)) \to (T <_{s} ({a ↾}_{dom T}) \leftrightarrow \neg (T = {a ↾}_{dom T} \lor ({a ↾}_{dom T}) <_{s} T))$
121	119 120	mpan	$⊢ (T \in No \land {a ↾}_{dom T} \in No) \to (T <_{s} ({a ↾}_{dom T}) \leftrightarrow \neg (T = {a ↾}_{dom T} \lor ({a ↾}_{dom T}) <_{s} T))$
122	93 118 121	syl2anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (T <_{s} ({a ↾}_{dom T}) \leftrightarrow \neg (T = {a ↾}_{dom T} \lor ({a ↾}_{dom T}) <_{s} T))$
123	122	con2bid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to ((T = {a ↾}_{dom T} \lor ({a ↾}_{dom T}) <_{s} T) \leftrightarrow \neg T <_{s} ({a ↾}_{dom T}))$
124	115 123	mpbird	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to (T = {a ↾}_{dom T} \lor ({a ↾}_{dom T}) <_{s} T)$
125	106 113 124	mpjaod	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T) \to a <_{s} W$
126	64	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to W \in No$
127	56	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to a \in No$
128		simplr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to a \neq W$
129	128	necomd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to W \neq a$
130	2	fveq1i	$⊢ W (⋂ \{p \in On \| a (p) \neq W (p)\}) = (T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})) (⋂ \{p \in On \| a (p) \neq W (p)\})$
131	92	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to T \in No$
132	131 94	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to Fun T$
133	132	funfnd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to T Fn dom T$
134		fnconstg	$⊢ 2_{𝑜} \in V \to ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) Fn (suc ⋃ bday [A] ∖ dom T)$
135	44 134	ax-mp	$⊢ ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) Fn (suc ⋃ bday [A] ∖ dom T)$
136	135	a1i	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) Fn (suc ⋃ bday [A] ∖ dom T)$
137		disjdif	$⊢ dom T \cap (suc ⋃ bday [A] ∖ dom T) = \emptyset$
138	137	a1i	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to dom T \cap (suc ⋃ bday [A] ∖ dom T) = \emptyset$
139		nosepssdm	$⊢ (a \in No \land W \in No \land a \neq W) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \subseteq dom a$
140	127 126 128 139	syl3anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \subseteq dom a$
141	127 15	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to bday (a) = dom a$
142		simp-5l	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to A \subseteq No$
143		simplrl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to a \in A$
144	143	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to a \in A$
145	19 142 144 20	mp3an2i	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to bday (a) \in bday [A]$
146		elssuni	$⊢ bday (a) \in bday [A] \to bday (a) \subseteq ⋃ bday [A]$
147	145 146	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to bday (a) \subseteq ⋃ bday [A]$
148	141 147	eqsstrrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to dom a \subseteq ⋃ bday [A]$
149	127 25 33	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to (dom a \subseteq ⋃ bday [A] \leftrightarrow dom a \in suc ⋃ bday [A])$
150	148 149	mpbid	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to dom a \in suc ⋃ bday [A]$
151		simpr	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to a \neq W$
152		nosepon	$⊢ (a \in No \land W \in No \land a \neq W) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in On$
153	56 64 151 152	syl3anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in On$
154	153	adantr	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in On$
155		eloni	$⊢ ⋂ \{p \in On \| a (p) \neq W (p)\} \in On \to Ord ⋂ \{p \in On \| a (p) \neq W (p)\}$
156		ordsuc	$⊢ Ord ⋃ bday [A] \leftrightarrow Ord suc ⋃ bday [A]$
157	31 156	mpbi	$⊢ Ord suc ⋃ bday [A]$
158		ordtr2	$⊢ (Ord ⋂ \{p \in On \| a (p) \neq W (p)\} \land Ord suc ⋃ bday [A]) \to ((⋂ \{p \in On \| a (p) \neq W (p)\} \subseteq dom a \land dom a \in suc ⋃ bday [A]) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in suc ⋃ bday [A])$
159	157 158	mpan2	$⊢ Ord ⋂ \{p \in On \| a (p) \neq W (p)\} \to ((⋂ \{p \in On \| a (p) \neq W (p)\} \subseteq dom a \land dom a \in suc ⋃ bday [A]) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in suc ⋃ bday [A])$
160	154 155 159	3syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to ((⋂ \{p \in On \| a (p) \neq W (p)\} \subseteq dom a \land dom a \in suc ⋃ bday [A]) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in suc ⋃ bday [A])$
161	140 150 160	mp2and	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in suc ⋃ bday [A]$
162		ontri1	$⊢ (dom T \in On \land ⋂ \{p \in On \| a (p) \neq W (p)\} \in On) \to (dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\} \leftrightarrow \neg ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T)$
163	109 153 162	syl2anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to (dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\} \leftrightarrow \neg ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T)$
164	163	biimpa	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to \neg ⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T$
165	161 164	eldifd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to ⋂ \{p \in On \| a (p) \neq W (p)\} \in (suc ⋃ bday [A] ∖ dom T)$
166	133 136 138 165	fvun2d	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to (T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})) (⋂ \{p \in On \| a (p) \neq W (p)\}) = ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) (⋂ \{p \in On \| a (p) \neq W (p)\})$
167	44	fvconst2	$⊢ ⋂ \{p \in On \| a (p) \neq W (p)\} \in (suc ⋃ bday [A] ∖ dom T) \to ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) (⋂ \{p \in On \| a (p) \neq W (p)\}) = 2_{𝑜}$
168	165 167	syl	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\}) (⋂ \{p \in On \| a (p) \neq W (p)\}) = 2_{𝑜}$
169	166 168	eqtrd	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to (T \cup ((suc ⋃ bday [A] ∖ dom T) \times \{2_{𝑜}\})) (⋂ \{p \in On \| a (p) \neq W (p)\}) = 2_{𝑜}$
170	130 169	syl5eq	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to W (⋂ \{p \in On \| a (p) \neq W (p)\}) = 2_{𝑜}$
171		nosep2o	$⊢ ((W \in No \land a \in No \land W \neq a) \land W (⋂ \{p \in On \| a (p) \neq W (p)\}) = 2_{𝑜}) \to a <_{s} W$
172	126 127 129 170 171	syl31anc	$⊢ (((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \land dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\}) \to a <_{s} W$
173	153 155	syl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to Ord ⋂ \{p \in On \| a (p) \neq W (p)\}$
174		nodmord	$⊢ T \in No \to Ord dom T$
175	92 174	syl	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to Ord dom T$
176		ordtri2or	$⊢ (Ord ⋂ \{p \in On \| a (p) \neq W (p)\} \land Ord dom T) \to (⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T \lor dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\})$
177	173 175 176	syl2anc	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to (⋂ \{p \in On \| a (p) \neq W (p)\} \in dom T \lor dom T \subseteq ⋂ \{p \in On \| a (p) \neq W (p)\})$
178	125 172 177	mpjaodan	$⊢ ((((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \land a \neq W) \to a <_{s} W$
179	54 178	mpdan	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land (a \in A \land \neg T <_{s} ({a ↾}_{dom T}))) \to a <_{s} W$
180	179	expr	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to (\neg T <_{s} ({a ↾}_{dom T}) \to a <_{s} W)$
181	8 180	sylbid	$⊢ (((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V)) \land a \in A) \to (\forall b \in B a <_{s} b \to a <_{s} W)$
182	181	ralimdva	$⊢ ((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 a \in A a <_{s} W)$
183	182	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 a \in A a <_{s} W$

Metamath Proof Explorer

Theorem noetainflem4

Proof