Theorem negsprop

Description: Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negsprop	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B )

Proof

Step	Hyp	Ref	Expression
1		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
2		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
3	1 2	onun2i	$$⊢\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\in \mathrm{On}$$
4		risset	$$⊢\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\in \mathrm{On}\leftrightarrow \exists a\in \mathrm{On}a=\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)$$
5	3 4	mpbi	$$⊢\exists a\in \mathrm{On}a=\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)$$
6		eqeq1	$$⊢a=b\to \left(a=\mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)\leftrightarrow b=\mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)\right)$$
7	6	imbi1d	Could not format ( a = b -> ( ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
8	7	2ralbidv	Could not format ( a = b -> ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) A. p e. No A. q e. No ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) A. p e. No A. q e. No ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
9		fveq2	$$⊢p=x\to \mathrm{bday}\left(p\right)=\mathrm{bday}\left(x\right)$$
10	9	uneq1d	$$⊢p=x\to \mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)=\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(q\right)$$
11	10	eqeq2d	$$⊢p=x\to \left(b=\mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)\leftrightarrow b=\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(q\right)\right)$$
12		fveq2	Could not format ( p = x -> ( -us ` p ) = ( -us ` x ) ) : No typesetting found for |- ( p = x -> ( -us ` p ) = ( -us ` x ) ) with typecode |-
13	12	eleq1d	Could not format ( p = x -> ( ( -us ` p ) e. No <-> ( -us ` x ) e. No ) ) : No typesetting found for |- ( p = x -> ( ( -us ` p ) e. No <-> ( -us ` x ) e. No ) ) with typecode |-
14		breq1	$$⊢p=x\to \left(p{<}_{s}q\leftrightarrow x{<}_{s}q\right)$$
15	12	breq2d	Could not format ( p = x -> ( ( -us ` q ) ( -us ` q ) ( ( -us ` q ) ( -us ` q )
16	14 15	imbi12d	Could not format ( p = x -> ( ( p ( -us ` q ) ( x ( -us ` q ) ( ( p ( -us ` q ) ( x ( -us ` q )
17	13 16	anbi12d	Could not format ( p = x -> ( ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` q ) ( ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` q )
18	11 17	imbi12d	Could not format ( p = x -> ( ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( b = ( ( bday ` x ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` q ) ( ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( b = ( ( bday ` x ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` q )
19		fveq2	$$⊢q=y\to \mathrm{bday}\left(q\right)=\mathrm{bday}\left(y\right)$$
20	19	uneq2d	$$⊢q=y\to \mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(q\right)=\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)$$
21	20	eqeq2d	$$⊢q=y\to \left(b=\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(q\right)\leftrightarrow b=\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\right)$$
22		breq2	$$⊢q=y\to \left(x{<}_{s}q\leftrightarrow x{<}_{s}y\right)$$
23		fveq2	Could not format ( q = y -> ( -us ` q ) = ( -us ` y ) ) : No typesetting found for |- ( q = y -> ( -us ` q ) = ( -us ` y ) ) with typecode |-
24	23	breq1d	Could not format ( q = y -> ( ( -us ` q ) ( -us ` y ) ( ( -us ` q ) ( -us ` y )
25	22 24	imbi12d	Could not format ( q = y -> ( ( x ( -us ` q ) ( x ( -us ` y ) ( ( x ( -us ` q ) ( x ( -us ` y )
26	25	anbi2d	Could not format ( q = y -> ( ( ( -us ` x ) e. No /\ ( x ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( -us ` x ) e. No /\ ( x ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y )
27	21 26	imbi12d	Could not format ( q = y -> ( ( b = ( ( bday ` x ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` q ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( b = ( ( bday ` x ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` q ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
28	18 27	cbvral2vw	Could not format ( A. p e. No A. q e. No ( b = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` p ) e. No /\ ( p ( -us ` q ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
29	8 28	bitrdi	Could not format ( a = b -> ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
30		raleq	Could not format ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
31		ralrot3	Could not format ( A. x e. No A. y e. No A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
32		r19.23v	Could not format ( A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( E. b e. ( ( bday ` p ) u. ( bday ` q ) ) b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( E. b e. ( ( bday ` p ) u. ( bday ` q ) ) b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
33		risset	$$⊢\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)\right)\leftrightarrow \exists b\in \left(\mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)\right)b=\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)$$
34	33	imbi1i	Could not format ( ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( E. b e. ( ( bday ` p ) u. ( bday ` q ) ) b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( E. b e. ( ( bday ` p ) u. ( bday ` q ) ) b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
35	32 34	bitr4i	Could not format ( A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
36	35	2ralbii	Could not format ( A. x e. No A. y e. No A. b e. ( ( bday ` p ) u. ( bday ` q ) ) ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
37	31 36	bitr3i	Could not format ( A. b e. ( ( bday ` p ) u. ( bday ` q ) ) A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
38	30 37	bitrdi	Could not format ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
39		simpr	Could not format ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
40		simpll	Could not format ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) p e. No ) : No typesetting found for |- ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) p e. No ) with typecode |-
41	39 40	negsproplem3	Could not format ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` p ) e. No /\ ( -us " ( _Right ` p ) ) < ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` p ) e. No /\ ( -us " ( _Right ` p ) ) <
42	41	simp1d	Could not format ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( -us ` p ) e. No ) : No typesetting found for |- ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( -us ` p ) e. No ) with typecode |-
43		simplr	Could not format ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
44		simplll	Could not format ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) p e. No ) : No typesetting found for |- ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) p e. No ) with typecode |-
45		simpllr	Could not format ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) q e. No ) : No typesetting found for |- ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) q e. No ) with typecode |-
46		simpr	Could not format ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) p ( ( -us ` x ) e. No /\ ( x ( -us ` y ) p
47	43 44 45 46	negsproplem7	Could not format ( ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( -us ` q )
48	47	ex	Could not format ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( p ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( p ( -us ` q )
49	42 48	jca	Could not format ( ( ( p e. No /\ q e. No ) /\ A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` p ) e. No /\ ( p ( -us ` q )
50	49	expcom	Could not format ( A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( p e. No /\ q e. No ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( p e. No /\ q e. No ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
51	38 50	syl6bi	Could not format ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( p e. No /\ q e. No ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( p e. No /\ q e. No ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
52	51	com3l	Could not format ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( p e. No /\ q e. No ) -> ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( p e. No /\ q e. No ) -> ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
53	52	ralrimivv	Could not format ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
54	53	a1i	Could not format ( a e. On -> ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( A. b e. a A. x e. No A. y e. No ( b = ( ( bday ` x ) u. ( bday ` y ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
55	29 54	tfis2	Could not format ( a e. On -> A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q )
56		fveq2	$$⊢p=A\to \mathrm{bday}\left(p\right)=\mathrm{bday}\left(A\right)$$
57	56	uneq1d	$$⊢p=A\to \mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)=\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(q\right)$$
58	57	eqeq2d	$$⊢p=A\to \left(a=\mathrm{bday}\left(p\right)\cup \mathrm{bday}\left(q\right)\leftrightarrow a=\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(q\right)\right)$$
59		fveq2	Could not format ( p = A -> ( -us ` p ) = ( -us ` A ) ) : No typesetting found for |- ( p = A -> ( -us ` p ) = ( -us ` A ) ) with typecode |-
60	59	eleq1d	Could not format ( p = A -> ( ( -us ` p ) e. No <-> ( -us ` A ) e. No ) ) : No typesetting found for |- ( p = A -> ( ( -us ` p ) e. No <-> ( -us ` A ) e. No ) ) with typecode |-
61		breq1	$$⊢p=A\to \left(p{<}_{s}q\leftrightarrow A{<}_{s}q\right)$$
62	59	breq2d	Could not format ( p = A -> ( ( -us ` q ) ( -us ` q ) ( ( -us ` q ) ( -us ` q )
63	61 62	imbi12d	Could not format ( p = A -> ( ( p ( -us ` q ) ( A ( -us ` q ) ( ( p ( -us ` q ) ( A ( -us ` q )
64	60 63	anbi12d	Could not format ( p = A -> ( ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` A ) e. No /\ ( A ( -us ` q ) ( ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( ( -us ` A ) e. No /\ ( A ( -us ` q )
65	58 64	imbi12d	Could not format ( p = A -> ( ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( a = ( ( bday ` A ) u. ( bday ` q ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` q ) ( ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( a = ( ( bday ` A ) u. ( bday ` q ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` q )
66		fveq2	$$⊢q=B\to \mathrm{bday}\left(q\right)=\mathrm{bday}\left(B\right)$$
67	66	uneq2d	$$⊢q=B\to \mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(q\right)=\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)$$
68	67	eqeq2d	$$⊢q=B\to \left(a=\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(q\right)\leftrightarrow a=\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
69		breq2	$$⊢q=B\to \left(A{<}_{s}q\leftrightarrow A{<}_{s}B\right)$$
70		fveq2	Could not format ( q = B -> ( -us ` q ) = ( -us ` B ) ) : No typesetting found for |- ( q = B -> ( -us ` q ) = ( -us ` B ) ) with typecode |-
71	70	breq1d	Could not format ( q = B -> ( ( -us ` q ) ( -us ` B ) ( ( -us ` q ) ( -us ` B )
72	69 71	imbi12d	Could not format ( q = B -> ( ( A ( -us ` q ) ( A ( -us ` B ) ( ( A ( -us ` q ) ( A ( -us ` B )
73	72	anbi2d	Could not format ( q = B -> ( ( ( -us ` A ) e. No /\ ( A ( -us ` q ) ( ( -us ` A ) e. No /\ ( A ( -us ` B ) ( ( ( -us ` A ) e. No /\ ( A ( -us ` q ) ( ( -us ` A ) e. No /\ ( A ( -us ` B )
74	68 73	imbi12d	Could not format ( q = B -> ( ( a = ( ( bday ` A ) u. ( bday ` q ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` q ) ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B ) ( ( a = ( ( bday ` A ) u. ( bday ` q ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` q ) ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B )
75	65 74	rspc2v	Could not format ( ( A e. No /\ B e. No ) -> ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B ) ( A. p e. No A. q e. No ( a = ( ( bday ` p ) u. ( bday ` q ) ) -> ( ( -us ` p ) e. No /\ ( p ( -us ` q ) ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B )
76	55 75	syl5com	Could not format ( a e. On -> ( ( A e. No /\ B e. No ) -> ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B ) ( ( A e. No /\ B e. No ) -> ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B )
77	76	com23	Could not format ( a e. On -> ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B ) ( a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B )
78	77	rexlimiv	Could not format ( E. a e. On a = ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B ) ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B )
79	5 78	ax-mp	Could not format ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) e. No /\ ( A ( -us ` B ) ( ( -us ` A ) e. No /\ ( A ( -us ` B )