Metamath Proof Explorer

Theorem madebday

Description: A surreal is part of the set made by ordinal A iff its birthday is less than or equal to A . Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion madebday ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 madebdayim ⊢ ( 𝑋 ∈ ( M ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ⊆ 𝐴 )
2 sseq2 ⊢ ( 𝑎 = 𝑏 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝑏 ) )
3 fveq2 ⊢ ( 𝑎 = 𝑏 → ( M ‘ 𝑎 ) = ( M ‘ 𝑏 ) )
4 3 eleq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ 𝑥 ∈ ( M ‘ 𝑏 ) ) )
5 2 4 imbi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ( ( bday ‘ 𝑥 ) ⊆ 𝑏 → 𝑥 ∈ ( M ‘ 𝑏 ) ) ) )
6 5 ralbidv ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝑏 → 𝑥 ∈ ( M ‘ 𝑏 ) ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑦 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) )
8 7 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( bday ‘ 𝑥 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑦 ) ⊆ 𝑏 ) )
9 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( M ‘ 𝑏 ) ↔ 𝑦 ∈ ( M ‘ 𝑏 ) ) )
10 8 9 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( bday ‘ 𝑥 ) ⊆ 𝑏 → 𝑥 ∈ ( M ‘ 𝑏 ) ) ↔ ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) )
11 10 cbvralvw ⊢ ( ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝑏 → 𝑥 ∈ ( M ‘ 𝑏 ) ) ↔ ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
12 6 11 bitrdi ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) )
13 sseq2 ⊢ ( 𝑎 = 𝐴 → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( bday ‘ 𝑥 ) ⊆ 𝐴 ) )
14 fveq2 ⊢ ( 𝑎 = 𝐴 → ( M ‘ 𝑎 ) = ( M ‘ 𝐴 ) )
15 14 eleq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑥 ∈ ( M ‘ 𝑎 ) ↔ 𝑥 ∈ ( M ‘ 𝐴 ) ) )
16 13 15 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ( ( bday ‘ 𝑥 ) ⊆ 𝐴 → 𝑥 ∈ ( M ‘ 𝐴 ) ) ) )
17 16 ralbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) ↔ ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝐴 → 𝑥 ∈ ( M ‘ 𝐴 ) ) ) )
18 bdayon ⊢ ( bday ‘ 𝑥 ) ∈ On
19 onsseleq ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ 𝑎 ∈ On ) → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( ( bday ‘ 𝑥 ) ∈ 𝑎 ∨ ( bday ‘ 𝑥 ) = 𝑎 ) ) )
20 18 19 mpan ⊢ ( 𝑎 ∈ On → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( ( bday ‘ 𝑥 ) ∈ 𝑎 ∨ ( bday ‘ 𝑥 ) = 𝑎 ) ) )
21 20 ad2antrr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 ↔ ( ( bday ‘ 𝑥 ) ∈ 𝑎 ∨ ( bday ‘ 𝑥 ) = 𝑎 ) ) )
22 simpll ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) → 𝑎 ∈ On )
23 onelss ⊢ ( 𝑎 ∈ On → ( ( bday ‘ 𝑥 ) ∈ 𝑎 → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
24 23 ad2antrr ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) → ( ( bday ‘ 𝑥 ) ∈ 𝑎 → ( bday ‘ 𝑥 ) ⊆ 𝑎 ) )
25 24 imp ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → ( bday ‘ 𝑥 ) ⊆ 𝑎 )
26 madess ⊢ ( ( 𝑎 ∈ On ∧ ( bday ‘ 𝑥 ) ⊆ 𝑎 ) → ( M ‘ ( bday ‘ 𝑥 ) ) ⊆ ( M ‘ 𝑎 ) )
27 22 25 26 syl2an2r ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → ( M ‘ ( bday ‘ 𝑥 ) ) ⊆ ( M ‘ 𝑎 ) )
28 ssid ⊢ ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝑥 )
29 simpr ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → ( bday ‘ 𝑥 ) ∈ 𝑎 )
30 simplr ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → 𝑥 ∈ No )
31 29 30 jca ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → ( ( bday ‘ 𝑥 ) ∈ 𝑎 ∧ 𝑥 ∈ No ) )
32 simpllr ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
33 sseq2 ⊢ ( 𝑏 = ( bday ‘ 𝑥 ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 ↔ ( bday ‘ 𝑦 ) ⊆ ( bday ‘ 𝑥 ) ) )
34 fveq2 ⊢ ( 𝑏 = ( bday ‘ 𝑥 ) → ( M ‘ 𝑏 ) = ( M ‘ ( bday ‘ 𝑥 ) ) )
35 34 eleq2d ⊢ ( 𝑏 = ( bday ‘ 𝑥 ) → ( 𝑦 ∈ ( M ‘ 𝑏 ) ↔ 𝑦 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) )
36 33 35 imbi12d ⊢ ( 𝑏 = ( bday ‘ 𝑥 ) → ( ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ↔ ( ( bday ‘ 𝑦 ) ⊆ ( bday ‘ 𝑥 ) → 𝑦 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) ) )
37 fveq2 ⊢ ( 𝑦 = 𝑥 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑥 ) )
38 37 sseq1d ⊢ ( 𝑦 = 𝑥 → ( ( bday ‘ 𝑦 ) ⊆ ( bday ‘ 𝑥 ) ↔ ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝑥 ) ) )
39 eleq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) )
40 38 39 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( ( bday ‘ 𝑦 ) ⊆ ( bday ‘ 𝑥 ) → 𝑦 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) ↔ ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝑥 ) → 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) ) )
41 36 40 rspc2v ⊢ ( ( ( bday ‘ 𝑥 ) ∈ 𝑎 ∧ 𝑥 ∈ No ) → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) → ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝑥 ) → 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) ) )
42 31 32 41 sylc ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → ( ( bday ‘ 𝑥 ) ⊆ ( bday ‘ 𝑥 ) → 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) )
43 28 42 mpi ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) )
44 27 43 sseldd ⊢ ( ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) ∧ ( bday ‘ 𝑥 ) ∈ 𝑎 ) → 𝑥 ∈ ( M ‘ 𝑎 ) )
45 44 ex ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) → ( ( bday ‘ 𝑥 ) ∈ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
46 madebdaylemlrcut ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑥 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
47 18 a1i ⊢ ( 𝑥 ∈ No → ( bday ‘ 𝑥 ) ∈ On )
48 lltr ⊢ ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 )
49 48 a1i ⊢ ( 𝑥 ∈ No → ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) )
50 leftssold ⊢ ( L ‘ 𝑥 ) ⊆ ( O ‘ ( bday ‘ 𝑥 ) )
51 50 a1i ⊢ ( 𝑥 ∈ No → ( L ‘ 𝑥 ) ⊆ ( O ‘ ( bday ‘ 𝑥 ) ) )
52 rightssold ⊢ ( R ‘ 𝑥 ) ⊆ ( O ‘ ( bday ‘ 𝑥 ) )
53 52 a1i ⊢ ( 𝑥 ∈ No → ( R ‘ 𝑥 ) ⊆ ( O ‘ ( bday ‘ 𝑥 ) ) )
54 madecut ⊢ ( ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) ) ∧ ( ( L ‘ 𝑥 ) ⊆ ( O ‘ ( bday ‘ 𝑥 ) ) ∧ ( R ‘ 𝑥 ) ⊆ ( O ‘ ( bday ‘ 𝑥 ) ) ) ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ∈ ( M ‘ ( bday ‘ 𝑥 ) ) )
55 47 49 51 53 54 syl22anc ⊢ ( 𝑥 ∈ No → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ∈ ( M ‘ ( bday ‘ 𝑥 ) ) )
56 55 adantl ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑥 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ∈ ( M ‘ ( bday ‘ 𝑥 ) ) )
57 46 56 eqeltrrd ⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑥 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) → 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) )
58 raleq ⊢ ( ( bday ‘ 𝑥 ) = 𝑎 → ( ∀ 𝑏 ∈ ( bday ‘ 𝑥 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) )
59 58 anbi1d ⊢ ( ( bday ‘ 𝑥 ) = 𝑎 → ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑥 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) ↔ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) ) )
60 fveq2 ⊢ ( ( bday ‘ 𝑥 ) = 𝑎 → ( M ‘ ( bday ‘ 𝑥 ) ) = ( M ‘ 𝑎 ) )
61 60 eleq2d ⊢ ( ( bday ‘ 𝑥 ) = 𝑎 → ( 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ↔ 𝑥 ∈ ( M ‘ 𝑎 ) ) )
62 59 61 imbi12d ⊢ ( ( bday ‘ 𝑥 ) = 𝑎 → ( ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑥 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) → 𝑥 ∈ ( M ‘ ( bday ‘ 𝑥 ) ) ) ↔ ( ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) → 𝑥 ∈ ( M ‘ 𝑎 ) ) ) )
63 57 62 mpbii ⊢ ( ( bday ‘ 𝑥 ) = 𝑎 → ( ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
64 63 com12 ⊢ ( ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑥 ∈ No ) → ( ( bday ‘ 𝑥 ) = 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
65 64 adantll ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) → ( ( bday ‘ 𝑥 ) = 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
66 45 65 jaod ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) → ( ( ( bday ‘ 𝑥 ) ∈ 𝑎 ∨ ( bday ‘ 𝑥 ) = 𝑎 ) → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
67 21 66 sylbid ⊢ ( ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) ∧ 𝑥 ∈ No ) → ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
68 67 ralrimiva ⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ) → ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) )
69 68 ex ⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) → ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝑎 → 𝑥 ∈ ( M ‘ 𝑎 ) ) ) )
70 12 17 69 tfis3 ⊢ ( 𝐴 ∈ On → ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝐴 → 𝑥 ∈ ( M ‘ 𝐴 ) ) )
71 fveq2 ⊢ ( 𝑥 = 𝑋 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑋 ) )
72 71 sseq1d ⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) ⊆ 𝐴 ↔ ( bday ‘ 𝑋 ) ⊆ 𝐴 ) )
73 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( M ‘ 𝐴 ) ↔ 𝑋 ∈ ( M ‘ 𝐴 ) ) )
74 72 73 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( bday ‘ 𝑥 ) ⊆ 𝐴 → 𝑥 ∈ ( M ‘ 𝐴 ) ) ↔ ( ( bday ‘ 𝑋 ) ⊆ 𝐴 → 𝑋 ∈ ( M ‘ 𝐴 ) ) ) )
75 74 rspccva ⊢ ( ( ∀ 𝑥 ∈ No ( ( bday ‘ 𝑥 ) ⊆ 𝐴 → 𝑥 ∈ ( M ‘ 𝐴 ) ) ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ⊆ 𝐴 → 𝑋 ∈ ( M ‘ 𝐴 ) ) )
76 70 75 sylan ⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ⊆ 𝐴 → 𝑋 ∈ ( M ‘ 𝐴 ) ) )
77 1 76 impbid2 ⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( M ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) ⊆ 𝐴 ) )