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