Metamath Proof Explorer

Theorem madebdaylemold

Description: Lemma for madebday . If the inductive hypothesis of madebday is satisfied, the converse of oldbdayim holds. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion madebdaylemold 
|- ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A -> X e. ( _Old ` A ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( y = X -> ( bday ` y ) = ( bday ` X ) )
2 1 sseq1d 
 |-  ( y = X -> ( ( bday ` y ) C_ b <-> ( bday ` X ) C_ b ) )
3 eleq1 
 |-  ( y = X -> ( y e. ( _M ` b ) <-> X e. ( _M ` b ) ) )
4 2 3 imbi12d 
 |-  ( y = X -> ( ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) <-> ( ( bday ` X ) C_ b -> X e. ( _M ` b ) ) ) )
5 4 rspcv 
 |-  ( X e. No -> ( A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) -> ( ( bday ` X ) C_ b -> X e. ( _M ` b ) ) ) )
6 5 ralimdv 
 |-  ( X e. No -> ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) -> A. b e. A ( ( bday ` X ) C_ b -> X e. ( _M ` b ) ) ) )
7 6 impcom 
 |-  ( ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> A. b e. A ( ( bday ` X ) C_ b -> X e. ( _M ` b ) ) )
8 rexim 
 |-  ( A. b e. A ( ( bday ` X ) C_ b -> X e. ( _M ` b ) ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _M ` b ) ) )
9 7 8 syl 
 |-  ( ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _M ` b ) ) )
10 9 3adant1 
 |-  ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _M ` b ) ) )
11 bdayelon 
 |-  ( bday ` X ) e. On
12 onelssex 
 |-  ( ( ( bday ` X ) e. On /\ A e. On ) -> ( ( bday ` X ) e. A <-> E. b e. A ( bday ` X ) C_ b ) )
13 11 12 mpan 
 |-  ( A e. On -> ( ( bday ` X ) e. A <-> E. b e. A ( bday ` X ) C_ b ) )
14 13 3ad2ant1 
 |-  ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A <-> E. b e. A ( bday ` X ) C_ b ) )
15 elold 
 |-  ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _M ` b ) ) )
16 15 3ad2ant1 
 |-  ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _M ` b ) ) )
17 10 14 16 3imtr4d 
 |-  ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A -> X e. ( _Old ` A ) ) )