# Metamath Proof Explorer

## Theorem nodense

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

Ref Expression
Assertion nodense ${⊢}\left(\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\wedge {A}{<}_{s}{B}\right)\right)\to \exists {x}\in \mathrm{No}\phantom{\rule{.4em}{0ex}}\left(\mathrm{bday}\left({x}\right)\in \mathrm{bday}\left({A}\right)\wedge {A}{<}_{s}{x}\wedge {x}{<}_{s}{B}\right)$

### Proof

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