nodense

Description: Given two distinct surreals with the same birthday, there is an older surreal lying between the two of them. Axiom SD of Alling p. 184. (Contributed by Scott Fenton, 16-Jun-2011)

		Ref	Expression
	Assertion	nodense	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to \exists x \in No (bday (x) \in bday (A) \land A <_{s} x \land x <_{s} B)$

Proof

Step	Hyp	Ref	Expression
1		nodenselem6	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \in No$
2		bdayval	$⊢ {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \in No \to bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) = dom ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}})$
3	1 2	syl	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) = dom ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}})$
4		dmres	$⊢ dom ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) = ⋂ \{a \in On \| A (a) \neq B (a)\} \cap dom A$
5		nodenselem5	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A)$
6		bdayfo	$⊢ bday : No \underset{onto}{⟶} On$
7		fof	$⊢ bday : No \underset{onto}{⟶} On \to bday : No ⟶ On$
8	6 7	ax-mp	$⊢ bday : No ⟶ On$
9		0elon	$⊢ \emptyset \in On$
10	8 9	f0cli	$⊢ bday (A) \in On$
11	10	onelssi	$⊢ ⋂ \{a \in On \| A (a) \neq B (a)\} \in bday (A) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \subseteq bday (A)$
12	5 11	syl	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \subseteq bday (A)$
13		bdayval	$⊢ A \in No \to bday (A) = dom A$
14	13	ad2antrr	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to bday (A) = dom A$
15	12 14	sseqtrd	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \subseteq dom A$
16		df-ss	$⊢ ⋂ \{a \in On \| A (a) \neq B (a)\} \subseteq dom A \leftrightarrow ⋂ \{a \in On \| A (a) \neq B (a)\} \cap dom A = ⋂ \{a \in On \| A (a) \neq B (a)\}$
17	15 16	sylib	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \cap dom A = ⋂ \{a \in On \| A (a) \neq B (a)\}$
18	4 17	syl5eq	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to dom ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) = ⋂ \{a \in On \| A (a) \neq B (a)\}$
19	3 18	eqtrd	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) = ⋂ \{a \in On \| A (a) \neq B (a)\}$
20	19 5	eqeltrd	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \in bday (A)$
21		nodenselem4	$⊢ ((A \in No \land B \in No) \land A <_{s} B) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
22	21	adantrl	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ⋂ \{a \in On \| A (a) \neq B (a)\} \in On$
23		nodenselem8	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \leftrightarrow (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
24	23	biimpd	$⊢ (A \in No \land B \in No \land bday (A) = bday (B)) \to (A <_{s} B \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
25	24	3expia	$⊢ (A \in No \land B \in No) \to (bday (A) = bday (B) \to (A <_{s} B \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})))$
26	25	imp32	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})$
27	26	simpld	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜}$
28		eqid	$⊢ \emptyset = \emptyset$
29	27 28	jctir	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land \emptyset = \emptyset)$
30	29	3mix1d	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land \emptyset = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land \emptyset = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land \emptyset = 2_{𝑜}))$
31		fvex	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \in V$
32		0ex	$⊢ \emptyset \in V$
33	31 32	brtp	$⊢ A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} \emptyset \leftrightarrow ((A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land \emptyset = \emptyset) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = 1_{𝑜} \land \emptyset = 2_{𝑜}) \lor (A (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset \land \emptyset = 2_{𝑜}))$
34	30 33	sylibr	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} \emptyset$
35	19	fveq2d	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}})) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\})$
36		fvnobday	$⊢ {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \in No \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}})) = \emptyset$
37	1 36	syl	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}})) = \emptyset$
38	35 37	eqtr3d	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset$
39	34 38	breqtrrd	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\})$
40		fvres	$⊢ y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = A (y)$
41	40	eqcomd	$⊢ y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y)$
42	41	rgen	$⊢ \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y)$
43	39 42	jctil	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}))$
44		raleq	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (\forall y \in x A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \leftrightarrow \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y))$
45		fveq2	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to A (x) = A (⋂ \{a \in On \| A (a) \neq B (a)\})$
46		fveq2	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\})$
47	45 46	breq12d	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) \leftrightarrow A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}))$
48	44 47	anbi12d	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to ((\forall y \in x A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x)) \leftrightarrow (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\})))$
49	48	rspcev	$⊢ (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}))) \to \exists x \in On (\forall y \in x A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x))$
50	22 43 49	syl2anc	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to \exists x \in On (\forall y \in x A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x))$
51		simpll	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to A \in No$
52		sltval	$⊢ (A \in No \land {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \in No) \to (A <_{s} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \leftrightarrow \exists x \in On (\forall y \in x A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x)))$
53	51 1 52	syl2anc	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to (A <_{s} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \leftrightarrow \exists x \in On (\forall y \in x A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) \land A (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x)))$
54	50 53	mpbird	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to A <_{s} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}})$
55	41	adantl	$⊢ (((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \land y \in ⋂ \{a \in On \| A (a) \neq B (a)\}) \to A (y) = ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y)$
56		nodenselem7	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to (y \in ⋂ \{a \in On \| A (a) \neq B (a)\} \to A (y) = B (y))$
57	56	imp	$⊢ (((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \land y \in ⋂ \{a \in On \| A (a) \neq B (a)\}) \to A (y) = B (y)$
58	55 57	eqtr3d	$⊢ (((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \land y \in ⋂ \{a \in On \| A (a) \neq B (a)\}) \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y)$
59	58	ralrimiva	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y)$
60	26	simprd	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}$
61	60 28	jctil	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to (\emptyset = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜})$
62	61	3mix3d	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ((\emptyset = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (\emptyset = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (\emptyset = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
63		fvex	$⊢ B (⋂ \{a \in On \| A (a) \neq B (a)\}) \in V$
64	32 63	brtp	$⊢ \emptyset \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}) \leftrightarrow ((\emptyset = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = \emptyset) \lor (\emptyset = 1_{𝑜} \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}) \lor (\emptyset = \emptyset \land B (⋂ \{a \in On \| A (a) \neq B (a)\}) = 2_{𝑜}))$
65	62 64	sylibr	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to \emptyset \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})$
66	38 65	eqbrtrd	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})$
67		raleq	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (\forall y \in x ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \leftrightarrow \forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y))$
68		fveq2	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to B (x) = B (⋂ \{a \in On \| A (a) \neq B (a)\})$
69	46 68	breq12d	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to (({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x) \leftrightarrow ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))$
70	67 69	anbi12d	$⊢ x = ⋂ \{a \in On \| A (a) \neq B (a)\} \to ((\forall y \in x ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)) \leftrightarrow (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\})))$
71	70	rspcev	$⊢ (⋂ \{a \in On \| A (a) \neq B (a)\} \in On \land (\forall y \in ⋂ \{a \in On \| A (a) \neq B (a)\} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (⋂ \{a \in On \| A (a) \neq B (a)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (⋂ \{a \in On \| A (a) \neq B (a)\}))) \to \exists x \in On (\forall y \in x ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
72	22 59 66 71	syl12anc	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to \exists x \in On (\forall y \in x ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x))$
73		simplr	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to B \in No$
74		sltval	$⊢ ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \in No \land B \in No) \to (({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) <_{s} B \leftrightarrow \exists x \in On (\forall y \in x ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$
75	1 73 74	syl2anc	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to (({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) <_{s} B \leftrightarrow \exists x \in On (\forall y \in x ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (y) = B (y) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) (x) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} B (x)))$
76	72 75	mpbird	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) <_{s} B$
77		fveq2	$⊢ x = {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \to bday (x) = bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}})$
78	77	eleq1d	$⊢ x = {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \to (bday (x) \in bday (A) \leftrightarrow bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \in bday (A))$
79		breq2	$⊢ x = {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \to (A <_{s} x \leftrightarrow A <_{s} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}))$
80		breq1	$⊢ x = {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \to (x <_{s} B \leftrightarrow ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) <_{s} B)$
81	78 79 80	3anbi123d	$⊢ x = {A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \to ((bday (x) \in bday (A) \land A <_{s} x \land x <_{s} B) \leftrightarrow (bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \in bday (A) \land A <_{s} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) <_{s} B))$
82	81	rspcev	$⊢ ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}} \in No \land (bday ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \in bday (A) \land A <_{s} ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) \land ({A ↾}_{⋂ \{a \in On \| A (a) \neq B (a)\}}) <_{s} B)) \to \exists x \in No (bday (x) \in bday (A) \land A <_{s} x \land x <_{s} B)$
83	1 20 54 76 82	syl13anc	$⊢ ((A \in No \land B \in No) \land (bday (A) = bday (B) \land A <_{s} B)) \to \exists x \in No (bday (x) \in bday (A) \land A <_{s} x \land x <_{s} B)$

Metamath Proof Explorer

Theorem nodense

Proof