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	Could not format assertion : No typesetting found for |- ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A -> X e. ( _Old ` A ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢y=X\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(X\right)$$
2	1	sseq1d	$$⊢y=X\to \left(\mathrm{bday}\left(y\right)\subseteq b\leftrightarrow \mathrm{bday}\left(X\right)\subseteq b\right)$$
3		eleq1	Could not format ( y = X -> ( y e. ( _Made ` b ) <-> X e. ( _Made ` b ) ) ) : No typesetting found for |- ( y = X -> ( y e. ( _Made ` b ) <-> X e. ( _Made ` b ) ) ) with typecode |-
4	2 3	imbi12d	Could not format ( y = X -> ( ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( y = X -> ( ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) ) with typecode |-
5	4	rspcv	Could not format ( X e. No -> ( A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( X e. No -> ( A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) ) with typecode |-
6	5	ralimdv	Could not format ( X e. No -> ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> A. b e. A ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( X e. No -> ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> A. b e. A ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) ) with typecode |-
7	6	impcom	Could not format ( ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> A. b e. A ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) : No typesetting found for |- ( ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> A. b e. A ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) ) with typecode |-
8		rexim	Could not format ( A. b e. A ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( A. b e. A ( ( bday ` X ) C_ b -> X e. ( _Made ` b ) ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
9	7 8	syl	Could not format ( ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( ( A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
10	9	3adant1	Could not format ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( E. b e. A ( bday ` X ) C_ b -> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
11		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
12		onelssex	$$⊢\left(\mathrm{bday}\left(X\right)\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(\mathrm{bday}\left(X\right)\in A\leftrightarrow \exists b\in A\mathrm{bday}\left(X\right)\subseteq b\right)$$
13	11 12	mpan	$$⊢A\in \mathrm{On}\to \left(\mathrm{bday}\left(X\right)\in A\leftrightarrow \exists b\in A\mathrm{bday}\left(X\right)\subseteq b\right)$$
14	13	3ad2ant1	Could not format ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A <-> E. b e. A ( bday ` X ) C_ b ) ) : No typesetting found for |- ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A <-> E. b e. A ( bday ` X ) C_ b ) ) with typecode |-
15		elold	Could not format ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
16	15	3ad2ant1	Could not format ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
17	10 14 16	3imtr4d	Could not format ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A -> X e. ( _Old ` A ) ) ) : No typesetting found for |- ( ( A e. On /\ A. b e. A A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( bday ` X ) e. A -> X e. ( _Old ` A ) ) ) with typecode |-