Theorem acexmidlemcase 5820

Description: Lemma for acexmid 5824. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle).

The cases are (1) the choice function evaluated at A equals { (/) }, (2) the choice function evaluated at B equals (/), and (3) the choice function evaluated at A equals (/) and the choice function evaluated at B equals { (/) }.

Because of the way we represent the choice function y, the choice function evaluated at A is ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) and the choice function evaluated at B is ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ). Other than the difference in notation these work just as ( y ` A ) and ( y ` B ) would if y were a function as defined by df-fun 5173.

Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at A equals { (/) }, then { (/) } e. A and likewise for B.

(Contributed by Jim Kingdon, 7-Aug-2019.)

Hypotheses

Ref	Expression
acexmidlem.a	|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }
acexmidlem.b	|- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }
acexmidlem.c	|- C = { A , B }

Assertion

Ref	Expression
acexmidlemcase	|- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( { (/) } e. A \/ (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )

Distinct variable groups:   x, y, z, v, u, A   x, B, y, z, v, u   x, C, y, z, v, u   ph, x, y, z, v, u

Proof of Theorem acexmidlemcase

Step	Hyp	Ref	Expression
1		acexmidlem.a	. . . . . . . . . . . . . 14 |- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }
2		onsucelsucexmidlem 4489	. . . . . . . . . . . . . 14 |- { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) } e. On
3	1, 2	eqeltri 2230	. . . . . . . . . . . . 13 |- A e. On
4		prid1g 3664	. . . . . . . . . . . . 13 |- ( A e. On -> A e. { A , B } )
5	3, 4	ax-mp 5	. . . . . . . . . . . 12 |- A e. { A , B }
6		acexmidlem.c	. . . . . . . . . . . 12 |- C = { A , B }
7	5, 6	eleqtrri 2233	. . . . . . . . . . 11 |- A e. C
8		eleq1 2220	. . . . . . . . . . . . . . 15 |- ( z = A -> ( z e. u <-> A e. u ) )
9	8	anbi1d 461	. . . . . . . . . . . . . 14 |- ( z = A -> ( ( z e. u /\ v e. u ) <-> ( A e. u /\ v e. u ) ) )
10	9	rexbidv 2458	. . . . . . . . . . . . 13 |- ( z = A -> ( E. u e. y ( z e. u /\ v e. u ) <-> E. u e. y ( A e. u /\ v e. u ) ) )
11	10	reueqd 2662	. . . . . . . . . . . 12 |- ( z = A -> ( E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E! v e. A E. u e. y ( A e. u /\ v e. u ) ) )
12	11	rspcv 2812	. . . . . . . . . . 11 |- ( A e. C -> ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> E! v e. A E. u e. y ( A e. u /\ v e. u ) ) )
13	7, 12	ax-mp 5	. . . . . . . . . 10 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> E! v e. A E. u e. y ( A e. u /\ v e. u ) )
14		riotacl 5795	. . . . . . . . . 10 |- ( E! v e. A E. u e. y ( A e. u /\ v e. u ) -> ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. A )
15	13, 14	syl 14	. . . . . . . . 9 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. A )
16		elrabi 2865	. . . . . . . . . 10 |- ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) } -> ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. { (/) , { (/) } } )
17	16, 1	eleq2s 2252	. . . . . . . . 9 |- ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. A -> ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. { (/) , { (/) } } )
18		elpri 3583	. . . . . . . . 9 |- ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. { (/) , { (/) } } -> ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) \/ ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = { (/) } ) )
19	15, 17, 18	3syl 17	. . . . . . . 8 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) \/ ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = { (/) } ) )
20		eleq1 2220	. . . . . . . . . 10 |- ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = { (/) } -> ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) e. A <-> { (/) } e. A ) )
21	15, 20	syl5ibcom 154	. . . . . . . . 9 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = { (/) } -> { (/) } e. A ) )
22	21	orim2d 778	. . . . . . . 8 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) \/ ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = { (/) } ) -> ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) \/ { (/) } e. A ) ) )
23	19, 22	mpd 13	. . . . . . 7 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) \/ { (/) } e. A ) )
24		acexmidlem.b	. . . . . . . . . . . . . 14 |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }
25		pp0ex 4151	. . . . . . . . . . . . . . 15 |- { (/) , { (/) } } e. _V
26	25	rabex 4109	. . . . . . . . . . . . . 14 |- { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) } e. _V
27	24, 26	eqeltri 2230	. . . . . . . . . . . . 13 |- B e. _V
28	27	prid2 3667	. . . . . . . . . . . 12 |- B e. { A , B }
29	28, 6	eleqtrri 2233	. . . . . . . . . . 11 |- B e. C
30		eleq1 2220	. . . . . . . . . . . . . . 15 |- ( z = B -> ( z e. u <-> B e. u ) )
31	30	anbi1d 461	. . . . . . . . . . . . . 14 |- ( z = B -> ( ( z e. u /\ v e. u ) <-> ( B e. u /\ v e. u ) ) )
32	31	rexbidv 2458	. . . . . . . . . . . . 13 |- ( z = B -> ( E. u e. y ( z e. u /\ v e. u ) <-> E. u e. y ( B e. u /\ v e. u ) ) )
33	32	reueqd 2662	. . . . . . . . . . . 12 |- ( z = B -> ( E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E! v e. B E. u e. y ( B e. u /\ v e. u ) ) )
34	33	rspcv 2812	. . . . . . . . . . 11 |- ( B e. C -> ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> E! v e. B E. u e. y ( B e. u /\ v e. u ) ) )
35	29, 34	ax-mp 5	. . . . . . . . . 10 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> E! v e. B E. u e. y ( B e. u /\ v e. u ) )
36		riotacl 5795	. . . . . . . . . 10 |- ( E! v e. B E. u e. y ( B e. u /\ v e. u ) -> ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. B )
37	35, 36	syl 14	. . . . . . . . 9 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. B )
38		elrabi 2865	. . . . . . . . . 10 |- ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) } -> ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. { (/) , { (/) } } )
39	38, 24	eleq2s 2252	. . . . . . . . 9 |- ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. B -> ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. { (/) , { (/) } } )
40		elpri 3583	. . . . . . . . 9 |- ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. { (/) , { (/) } } -> ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = (/) \/ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) )
41	37, 39, 40	3syl 17	. . . . . . . 8 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = (/) \/ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) )
42		eleq1 2220	. . . . . . . . . 10 |- ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = (/) -> ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) e. B <-> (/) e. B ) )
43	37, 42	syl5ibcom 154	. . . . . . . . 9 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = (/) -> (/) e. B ) )
44	43	orim1d 777	. . . . . . . 8 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = (/) \/ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) -> ( (/) e. B \/ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )
45	41, 44	mpd 13	. . . . . . 7 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( (/) e. B \/ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) )
46	23, 45	jca 304	. . . . . 6 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) \/ { (/) } e. A ) /\ ( (/) e. B \/ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )
47		anddi 811	. . . . . 6 |- ( ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) \/ { (/) } e. A ) /\ ( (/) e. B \/ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) <-> ( ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) \/ ( ( { (/) } e. A /\ (/) e. B ) \/ ( { (/) } e. A /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) )
48	46, 47	sylib 121	. . . . 5 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) \/ ( ( { (/) } e. A /\ (/) e. B ) \/ ( { (/) } e. A /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) )
49		simpl 108	. . . . . . 7 |- ( ( { (/) } e. A /\ (/) e. B ) -> { (/) } e. A )
50		simpl 108	. . . . . . 7 |- ( ( { (/) } e. A /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) -> { (/) } e. A )
51	49, 50	jaoi 706	. . . . . 6 |- ( ( ( { (/) } e. A /\ (/) e. B ) \/ ( { (/) } e. A /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) -> { (/) } e. A )
52	51	orim2i 751	. . . . 5 |- ( ( ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) \/ ( ( { (/) } e. A /\ (/) e. B ) \/ ( { (/) } e. A /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) -> ( ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) \/ { (/) } e. A ) )
53	48, 52	syl 14	. . . 4 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) \/ { (/) } e. A ) )
54	53	orcomd 719	. . 3 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( { (/) } e. A \/ ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) )
55		simpr 109	. . . . 5 |- ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) -> (/) e. B )
56	55	orim1i 750	. . . 4 |- ( ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) -> ( (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )
57	56	orim2i 751	. . 3 |- ( ( { (/) } e. A \/ ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ (/) e. B ) \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) -> ( { (/) } e. A \/ ( (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) )
58	54, 57	syl 14	. 2 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( { (/) } e. A \/ ( (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) )
59		3orass 966	. 2 |- ( ( { (/) } e. A \/ (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) <-> ( { (/) } e. A \/ ( (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) ) )
60	58, 59	sylibr 133	1 |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( { (/) } e. A \/ (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 698   \/ w3o 962   = wceq 1335   e. wcel 2128   A.wral 2435   E.wrex 2436   E!wreu 2437   {crab 2439   _Vcvv 2712   (/)c0 3394   {csn 3560   {cpr 3561   Oncon0 4324   iota_crio 5780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4083  ax-nul 4091  ax-pow 4136

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-uni 3774  df-tr 4064  df-iord 4327  df-on 4329  df-suc 4332  df-iota 5136  df-riota 5781

This theorem is referenced by:  acexmidlem1  5821