Metamath Proof Explorer

Theorem nodenselem8

Description: Lemma for nodense . Give a condition for surreal less than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011)

Ref Expression
Assertion 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)$

Proof

Step Hyp Ref Expression
1 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)$
2 1 exp32 ${⊢}\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 \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\right)$
3 2 3impia ${⊢}\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 \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)$
4 sltval2 ${⊢}\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\right)\to \left({A}{<}_{s}{B}↔{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\}{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\right)$
5 4 3adant3 ${⊢}\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}↔{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\}{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\right)$
6 fvex ${⊢}{A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\in \mathrm{V}$
7 fvex ${⊢}{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\in \mathrm{V}$
8 6 7 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\}{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)↔\left(\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)=\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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\right)\right)$
9 eleq2 ${⊢}\mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\to \left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)↔\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\right)$
10 9 biimpd ${⊢}\mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\to \left(\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\}\in \mathrm{bday}\left({B}\right)\right)$
11 nosgnn0 ${⊢}¬\varnothing \in \left\{{1}_{𝑜},{2}_{𝑜}\right\}$
12 nofnbday ${⊢}{B}\in \mathrm{No}\to {B}Fn\mathrm{bday}\left({B}\right)$
13 fnfvelrn ${⊢}\left({B}Fn\mathrm{bday}\left({B}\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\right)\to {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\in \mathrm{ran}{B}$
14 eleq1 ${⊢}{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \left({B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\in \mathrm{ran}{B}↔\varnothing \in \mathrm{ran}{B}\right)$
15 13 14 syl5ibcom ${⊢}\left({B}Fn\mathrm{bday}\left({B}\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\right)\to \left({B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \varnothing \in \mathrm{ran}{B}\right)$
16 12 15 sylan ${⊢}\left({B}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\right)\to \left({B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \varnothing \in \mathrm{ran}{B}\right)$
17 norn ${⊢}{B}\in \mathrm{No}\to \mathrm{ran}{B}\subseteq \left\{{1}_{𝑜},{2}_{𝑜}\right\}$
18 17 sseld ${⊢}{B}\in \mathrm{No}\to \left(\varnothing \in \mathrm{ran}{B}\to \varnothing \in \left\{{1}_{𝑜},{2}_{𝑜}\right\}\right)$
19 18 adantr ${⊢}\left({B}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\right)\to \left(\varnothing \in \mathrm{ran}{B}\to \varnothing \in \left\{{1}_{𝑜},{2}_{𝑜}\right\}\right)$
20 16 19 syld ${⊢}\left({B}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\right)\to \left({B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \varnothing \in \left\{{1}_{𝑜},{2}_{𝑜}\right\}\right)$
21 11 20 mtoi ${⊢}\left({B}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\right)\to ¬{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing$
22 21 ex ${⊢}{B}\in \mathrm{No}\to \left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\to ¬{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \right)$
23 22 adantl ${⊢}\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\right)\to \left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({B}\right)\to ¬{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \right)$
24 10 23 syl9r ${⊢}\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(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\to ¬{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \right)\right)$
25 24 3impia ${⊢}\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\to \left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\to ¬{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \right)$
26 25 imp ${⊢}\left(\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to ¬{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing$
27 26 intnand ${⊢}\left(\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\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)=\varnothing \right)$
28 nofnbday ${⊢}{A}\in \mathrm{No}\to {A}Fn\mathrm{bday}\left({A}\right)$
29 fnfvelrn ${⊢}\left({A}Fn\mathrm{bday}\left({A}\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to {A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\in \mathrm{ran}{A}$
30 eleq1 ${⊢}{A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \left({A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)\in \mathrm{ran}{A}↔\varnothing \in \mathrm{ran}{A}\right)$
31 29 30 syl5ibcom ${⊢}\left({A}Fn\mathrm{bday}\left({A}\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to \left({A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \varnothing \in \mathrm{ran}{A}\right)$
32 28 31 sylan ${⊢}\left({A}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to \left({A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \varnothing \in \mathrm{ran}{A}\right)$
33 norn ${⊢}{A}\in \mathrm{No}\to \mathrm{ran}{A}\subseteq \left\{{1}_{𝑜},{2}_{𝑜}\right\}$
34 33 sseld ${⊢}{A}\in \mathrm{No}\to \left(\varnothing \in \mathrm{ran}{A}\to \varnothing \in \left\{{1}_{𝑜},{2}_{𝑜}\right\}\right)$
35 34 adantr ${⊢}\left({A}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to \left(\varnothing \in \mathrm{ran}{A}\to \varnothing \in \left\{{1}_{𝑜},{2}_{𝑜}\right\}\right)$
36 32 35 syld ${⊢}\left({A}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to \left({A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \to \varnothing \in \left\{{1}_{𝑜},{2}_{𝑜}\right\}\right)$
37 11 36 mtoi ${⊢}\left({A}\in \mathrm{No}\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to ¬{A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing$
38 37 3ad2antl1 ${⊢}\left(\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to ¬{A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing$
39 38 intnanrd ${⊢}\left(\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to ¬\left({A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \wedge {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\right)$
40 3orel13 ${⊢}\left(¬\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)=\varnothing \right)\wedge ¬\left({A}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)=\varnothing \wedge {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\right)\right)\to \left(\left(\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)=\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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\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)\right)$
41 27 39 40 syl2anc ${⊢}\left(\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\wedge \bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\right)\to \left(\left(\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)=\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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\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)\right)$
42 41 ex ${⊢}\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\to \left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\right)\to \left(\left(\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)=\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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\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)\right)\right)$
43 42 com23 ${⊢}\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({B}\right)\right)\to \left(\left(\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)=\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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\right)\right)\to \left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\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)\right)\right)$
44 8 43 syl5bi ${⊢}\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}\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)\to \left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\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)\right)\right)$
45 5 44 sylbid ${⊢}\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(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\in \mathrm{bday}\left({A}\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)\right)\right)$
46 3 45 mpdd ${⊢}\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)$
47 3mix2 ${⊢}\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)\to \left(\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)=\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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\right)\right)$
48 47 8 sylibr ${⊢}\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)\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\}{B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)$
49 48 5 syl5ibr ${⊢}\left({A}\in \mathrm{No}\wedge {B}\in \mathrm{No}\wedge \mathrm{bday}\left({A}\right)=\mathrm{bday}\left({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 {B}\left(\bigcap \left\{{a}\in \mathrm{On}|{A}\left({a}\right)\ne {B}\left({a}\right)\right\}\right)={2}_{𝑜}\right)\to {A}{<}_{s}{B}\right)$
50 46 49 impbid ${⊢}\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)$