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	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nodenselem6	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No )
2		bdayval	⊢ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No → ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) = dom ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
3	1 2	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) = dom ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
4		dmres	⊢ dom ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∩ dom 𝐴 )
5		nodenselem5	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ ( bday ‘ 𝐴 ) )
6		bdayfo	⊢ bday : No –onto→ On
7		fof	⊢ ( bday : No –onto→ On → bday : No ⟶ On )
8	6 7	ax-mp	⊢ bday : No ⟶ On
9		0elon	⊢ ∅ ∈ On
10	8 9	f0cli	⊢ ( bday ‘ 𝐴 ) ∈ On
11	10	onelssi	⊢ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ ( bday ‘ 𝐴 ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ ( bday ‘ 𝐴 ) )
12	5 11	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ ( bday ‘ 𝐴 ) )
13		bdayval	⊢ ( 𝐴 ∈ No → ( bday ‘ 𝐴 ) = dom 𝐴 )
14	13	ad2antrr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ 𝐴 ) = dom 𝐴 )
15	12 14	sseqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ dom 𝐴 )
16		dfss2	⊢ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ⊆ dom 𝐴 ↔ ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∩ dom 𝐴 ) = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } )
17	15 16	sylib	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∩ dom 𝐴 ) = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } )
18	4 17	eqtrid	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → dom ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } )
19	3 18	eqtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } )
20	19 5	eqeltrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ∈ ( bday ‘ 𝐴 ) )
21		nodenselem4	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵 ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On )
22	21	adantrl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On )
23		nodenselem8	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( 𝐴 <s 𝐵 ↔ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) ) )
24	23	biimpd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( 𝐴 <s 𝐵 → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) ) )
25	24	3expia	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) → ( 𝐴 <s 𝐵 → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) ) ) )
26	25	imp32	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) )
27	26	simpld	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o )
28		eqid	⊢ ∅ = ∅
29	27 28	jctir	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ∅ = ∅ ) )
30	29	3mix1d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ∅ = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ∅ = 2_o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ∧ ∅ = 2_o ) ) )
31		fvex	⊢ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ V
32		0ex	⊢ ∅ ∈ V
33	31 32	brtp	⊢ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ∅ ↔ ( ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ∅ = ∅ ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 1_o ∧ ∅ = 2_o ) ∨ ( ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ∧ ∅ = 2_o ) ) )
34	30 33	sylibr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ∅ )
35	19	fveq2d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
36		fvnobday	⊢ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) = ∅ )
37	1 36	syl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) = ∅ )
38	35 37	eqtr3d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ )
39	34 38	breqtrrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
40		fvres	⊢ ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
41	40	eqcomd	⊢ ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) )
42	41	rgen	⊢ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 )
43	39 42	jctil	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) )
44		raleq	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ) )
45		fveq2	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
46		fveq2	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
47	45 46	breq12d	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( 𝐴 ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) ↔ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) )
48	44 47	anbi12d	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) )
49	48	rspcev	⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) ) )
50	22 43 49	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) ) )
51		simpll	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 ∈ No )
52		ltsval	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No ) → ( 𝐴 <s ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) ) ) )
53	51 1 52	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 <s ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) ) ) )
54	50 53	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 <s ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
55	41	adantl	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) )
56		nodenselem7	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) )
57	56	imp	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝐴 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
58	55 57	eqtr3d	⊢ ( ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) ∧ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
59	58	ralrimiva	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) )
60	26	simprd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o )
61	60 28	jctil	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ∅ = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) )
62	61	3mix3d	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( ∅ = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) ∨ ( ∅ = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) ∨ ( ∅ = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) ) )
63		fvex	⊢ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ V
64	32 63	brtp	⊢ ( ∅ { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ↔ ( ( ∅ = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = ∅ ) ∨ ( ∅ = 1_o ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) ∨ ( ∅ = ∅ ∧ ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) = 2_o ) ) )
65	62 64	sylibr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∅ { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
66	38 65	eqbrtrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
67		raleq	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ) )
68		fveq2	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) )
69	46 68	breq12d	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ 𝑥 ) ↔ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) )
70	67 69	anbi12d	⊢ ( 𝑥 = ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } → ( ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) )
71	70	rspcev	⊢ ( ( ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ∈ On ∧ ( ∀ 𝑦 ∈ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
72	22 59 66 71	syl12anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ 𝑥 ) ) )
73		simplr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐵 ∈ No )
74		ltsval	⊢ ( ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
75	1 73 74	syl2anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵 ‘ 𝑦 ) ∧ ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ ∅ , 2_o ⟩ } ( 𝐵 ‘ 𝑥 ) ) ) )
76	72 75	mpbird	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) <s 𝐵 )
77		fveq2	⊢ ( 𝑥 = ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( bday ‘ 𝑥 ) = ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) )
78	77	eleq1d	⊢ ( 𝑥 = ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ↔ ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ∈ ( bday ‘ 𝐴 ) ) )
79		breq2	⊢ ( 𝑥 = ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝐴 <s 𝑥 ↔ 𝐴 <s ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) )
80		breq1	⊢ ( 𝑥 = ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( 𝑥 <s 𝐵 ↔ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) <s 𝐵 ) )
81	78 79 80	3anbi123d	⊢ ( 𝑥 = ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) → ( ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵 ) ↔ ( ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∧ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) <s 𝐵 ) ) )
82	81	rspcev	⊢ ( ( ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∈ No ∧ ( ( bday ‘ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) ∧ ( 𝐴 ↾ ∩ { 𝑎 ∈ On ∣ ( 𝐴 ‘ 𝑎 ) ≠ ( 𝐵 ‘ 𝑎 ) } ) <s 𝐵 ) ) → ∃ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵 ) )
83	1 20 54 76 82	syl13anc	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵 ) )

Metamath Proof Explorer

Theorem nodense

Proof