Step |
Hyp |
Ref |
Expression |
1 |
|
simp2l |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝐴 <<s { 𝑋 } ) |
2 |
|
simp2r |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → { 𝑋 } <<s 𝐵 ) |
3 |
|
snnzg |
⊢ ( 𝑋 ∈ No → { 𝑋 } ≠ ∅ ) |
4 |
3
|
3ad2ant1 |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → { 𝑋 } ≠ ∅ ) |
5 |
|
sslttr |
⊢ ( ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ∧ { 𝑋 } ≠ ∅ ) → 𝐴 <<s 𝐵 ) |
6 |
1 2 4 5
|
syl3anc |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝐴 <<s 𝐵 ) |
7 |
|
scutbday |
⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
8 |
6 7
|
syl |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
9 |
|
bdayfn |
⊢ bday Fn No |
10 |
|
ssrab2 |
⊢ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No |
11 |
|
simp1 |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝑋 ∈ No ) |
12 |
|
simp2 |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) |
13 |
|
sneq |
⊢ ( 𝑦 = 𝑋 → { 𝑦 } = { 𝑋 } ) |
14 |
13
|
breq2d |
⊢ ( 𝑦 = 𝑋 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑋 } ) ) |
15 |
13
|
breq1d |
⊢ ( 𝑦 = 𝑋 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑋 } <<s 𝐵 ) ) |
16 |
14 15
|
anbi12d |
⊢ ( 𝑦 = 𝑋 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ) |
17 |
16
|
elrab |
⊢ ( 𝑋 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ) |
18 |
11 12 17
|
sylanbrc |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → 𝑋 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) |
19 |
|
fnfvima |
⊢ ( ( bday Fn No ∧ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No ∧ 𝑋 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
20 |
9 10 18 19
|
mp3an12i |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
21 |
|
intss1 |
⊢ ( ( bday ‘ 𝑋 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑋 ) ) |
22 |
20 21
|
syl |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑋 ) ) |
23 |
8 22
|
eqsstrd |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑋 ) ) |
24 |
|
simprl |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → 𝐴 <<s { 𝑋 } ) |
25 |
|
simprr |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → { 𝑋 } <<s 𝐵 ) |
26 |
3
|
adantr |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → { 𝑋 } ≠ ∅ ) |
27 |
24 25 26 5
|
syl3anc |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → 𝐴 <<s 𝐵 ) |
28 |
27 7
|
syl |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
29 |
28
|
eqeq1d |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ↔ ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) = ( bday ‘ 𝑋 ) ) ) |
30 |
|
eqcom |
⊢ ( ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) = ( bday ‘ 𝑋 ) ↔ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
31 |
29 30
|
bitrdi |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ↔ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
32 |
31
|
biimpa |
⊢ ( ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ) → ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
33 |
17
|
biimpri |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → 𝑋 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) |
34 |
27
|
adantr |
⊢ ( ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ) → 𝐴 <<s 𝐵 ) |
35 |
|
conway |
⊢ ( 𝐴 <<s 𝐵 → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
36 |
34 35
|
syl |
⊢ ( ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ) → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) |
37 |
|
fveqeq2 |
⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
38 |
37
|
riota2 |
⊢ ( ( 𝑋 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∧ ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) → ( ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) = 𝑋 ) ) |
39 |
|
eqcom |
⊢ ( ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) = 𝑋 ↔ 𝑋 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
40 |
38 39
|
bitrdi |
⊢ ( ( 𝑋 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∧ ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) → ( ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ 𝑋 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) ) |
41 |
33 36 40
|
syl2an2r |
⊢ ( ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ) → ( ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ 𝑋 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) ) |
42 |
32 41
|
mpbid |
⊢ ( ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ) → 𝑋 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
43 |
|
scutval |
⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
44 |
34 43
|
syl |
⊢ ( ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ) → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ) |
45 |
42 44
|
eqtr4d |
⊢ ( ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) ) → 𝑋 = ( 𝐴 |s 𝐵 ) ) |
46 |
45
|
ex |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ( bday ‘ 𝑋 ) → 𝑋 = ( 𝐴 |s 𝐵 ) ) ) |
47 |
46
|
necon3d |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ) → ( 𝑋 ≠ ( 𝐴 |s 𝐵 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday ‘ 𝑋 ) ) ) |
48 |
47
|
3impia |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday ‘ 𝑋 ) ) |
49 |
|
bdayelon |
⊢ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On |
50 |
|
bdayelon |
⊢ ( bday ‘ 𝑋 ) ∈ On |
51 |
|
onelpss |
⊢ ( ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑋 ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday ‘ 𝑋 ) ) ) ) |
52 |
49 50 51
|
mp2an |
⊢ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑋 ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ ( bday ‘ 𝑋 ) ) ) |
53 |
23 48 52
|
sylanbrc |
⊢ ( ( 𝑋 ∈ No ∧ ( 𝐴 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝐵 ) ∧ 𝑋 ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ 𝑋 ) ) |