Theorem exmidaclem 7224

Description: Lemma for exmidac 7225. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)

Hypotheses

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

Assertion

Ref	Expression
exmidaclem	|- (CHOICE -> EXMID )

Distinct variable groups:   x, A   x, B   x, y

Allowed substitution hints:   A( y)   B( y)   C( x, y)

Proof of Theorem exmidaclem

Dummy variables z f w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 109	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> CHOICE )
2		exmidaclem.c	. . . . . 6 |- C = { A , B }
3		exmidaclem.a	. . . . . . . 8 |- A = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) }
4		pp0ex 4203	. . . . . . . . 9 |- { (/) , { (/) } } e. _V
5	4	rabex 4161	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } e. _V
6	3, 5	eqeltri 2261	. . . . . . 7 |- A e. _V
7		exmidaclem.b	. . . . . . . 8 |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }
8	4	rabex 4161	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } e. _V
9	7, 8	eqeltri 2261	. . . . . . 7 |- B e. _V
10		prexg 4225	. . . . . . 7 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
11	6, 9, 10	mp2an 426	. . . . . 6 |- { A , B } e. _V
12	2, 11	eqeltri 2261	. . . . 5 |- C e. _V
13	12	a1i 9	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> C e. _V )
14		simpr 110	. . . . . . 7 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> z e. C )
15	14, 2	eleqtrdi 2281	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> z e. { A , B } )
16		elpri 3629	. . . . . 6 |- ( z e. { A , B } -> ( z = A \/ z = B ) )
17		0ex 4144	. . . . . . . . . . 11 |- (/) e. _V
18	17	prid1 3712	. . . . . . . . . 10 |- (/) e. { (/) , { (/) } }
19		eqid 2188	. . . . . . . . . . 11 |- (/) = (/)
20	19	orci 732	. . . . . . . . . 10 |- ( (/) = (/) \/ y = { (/) } )
21		eqeq1 2195	. . . . . . . . . . . 12 |- ( x = (/) -> ( x = (/) <-> (/) = (/) ) )
22	21	orbi1d 792	. . . . . . . . . . 11 |- ( x = (/) -> ( ( x = (/) \/ y = { (/) } ) <-> ( (/) = (/) \/ y = { (/) } ) ) )
23	22, 3	elrab2 2910	. . . . . . . . . 10 |- ( (/) e. A <-> ( (/) e. { (/) , { (/) } } /\ ( (/) = (/) \/ y = { (/) } ) ) )
24	18, 20, 23	mpbir2an 943	. . . . . . . . 9 |- (/) e. A
25		eleq2 2252	. . . . . . . . 9 |- ( z = A -> ( (/) e. z <-> (/) e. A ) )
26	24, 25	mpbiri 168	. . . . . . . 8 |- ( z = A -> (/) e. z )
27		elex2 2767	. . . . . . . 8 |- ( (/) e. z -> E. w w e. z )
28	26, 27	syl 14	. . . . . . 7 |- ( z = A -> E. w w e. z )
29		p0ex 4202	. . . . . . . . . . 11 |- { (/) } e. _V
30	29	prid2 3713	. . . . . . . . . 10 |- { (/) } e. { (/) , { (/) } }
31		eqid 2188	. . . . . . . . . . 11 |- { (/) } = { (/) }
32	31	orci 732	. . . . . . . . . 10 |- ( { (/) } = { (/) } \/ y = { (/) } )
33		eqeq1 2195	. . . . . . . . . . . 12 |- ( x = { (/) } -> ( x = { (/) } <-> { (/) } = { (/) } ) )
34	33	orbi1d 792	. . . . . . . . . . 11 |- ( x = { (/) } -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( { (/) } = { (/) } \/ y = { (/) } ) ) )
35	34, 7	elrab2 2910	. . . . . . . . . 10 |- ( { (/) } e. B <-> ( { (/) } e. { (/) , { (/) } } /\ ( { (/) } = { (/) } \/ y = { (/) } ) ) )
36	30, 32, 35	mpbir2an 943	. . . . . . . . 9 |- { (/) } e. B
37		eleq2 2252	. . . . . . . . 9 |- ( z = B -> ( { (/) } e. z <-> { (/) } e. B ) )
38	36, 37	mpbiri 168	. . . . . . . 8 |- ( z = B -> { (/) } e. z )
39		elex2 2767	. . . . . . . 8 |- ( { (/) } e. z -> E. w w e. z )
40	38, 39	syl 14	. . . . . . 7 |- ( z = B -> E. w w e. z )
41	28, 40	jaoi 717	. . . . . 6 |- ( ( z = A \/ z = B ) -> E. w w e. z )
42	15, 16, 41	3syl 17	. . . . 5 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> E. w w e. z )
43	42	ralrimiva 2562	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> A. z e. C E. w w e. z )
44	1, 13, 43	acfun 7223	. . 3 |- ( (CHOICE /\ y C_ { (/) } ) -> E. f ( f Fn C /\ A. z e. C ( f ` z ) e. z ) )
45		0nep0 4179	. . . . . . . . . 10 |- (/) =/= { (/) }
46	45	neii 2361	. . . . . . . . 9 |- -. (/) = { (/) }
47		simplr 528	. . . . . . . . . 10 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> ( f ` A ) = (/) )
48		simpr 110	. . . . . . . . . 10 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> ( f ` B ) = { (/) } )
49	47, 48	eqeq12d 2203	. . . . . . . . 9 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> ( ( f ` A ) = ( f ` B ) <-> (/) = { (/) } ) )
50	46, 49	mtbiri 676	. . . . . . . 8 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> -. ( f ` A ) = ( f ` B ) )
51		olc 712	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = (/) \/ y = { (/) } ) )
52	51	ralrimivw 2563	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = (/) \/ y = { (/) } ) )
53		rabid2 2666	. . . . . . . . . . . 12 |- ( { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } <-> A. x e. { (/) , { (/) } } ( x = (/) \/ y = { (/) } ) )
54	52, 53	sylibr 134	. . . . . . . . . . 11 |- ( y = { (/) } -> { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } )
55	54, 3	eqtr4di 2239	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = A )
56		olc 712	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = { (/) } \/ y = { (/) } ) )
57	56	ralrimivw 2563	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = { (/) } \/ y = { (/) } ) )
58		rabid2 2666	. . . . . . . . . . . 12 |- ( { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } <-> A. x e. { (/) , { (/) } } ( x = { (/) } \/ y = { (/) } ) )
59	57, 58	sylibr 134	. . . . . . . . . . 11 |- ( y = { (/) } -> { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } )
60	59, 7	eqtr4di 2239	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = B )
61	55, 60	eqtr3d 2223	. . . . . . . . 9 |- ( y = { (/) } -> A = B )
62	61	fveq2d 5533	. . . . . . . 8 |- ( y = { (/) } -> ( f ` A ) = ( f ` B ) )
63	50, 62	nsyl 629	. . . . . . 7 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> -. y = { (/) } )
64	63	olcd 735	. . . . . 6 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
65		simpr 110	. . . . . . 7 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ y = { (/) } ) -> y = { (/) } )
66	65	orcd 734	. . . . . 6 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ y = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
67		fveq2 5529	. . . . . . . . . . 11 |- ( z = B -> ( f ` z ) = ( f ` B ) )
68		id 19	. . . . . . . . . . 11 |- ( z = B -> z = B )
69	67, 68	eleq12d 2259	. . . . . . . . . 10 |- ( z = B -> ( ( f ` z ) e. z <-> ( f ` B ) e. B ) )
70		simprr 531	. . . . . . . . . 10 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> A. z e. C ( f ` z ) e. z )
71	9	prid2 3713	. . . . . . . . . . . 12 |- B e. { A , B }
72	71, 2	eleqtrri 2264	. . . . . . . . . . 11 |- B e. C
73	72	a1i 9	. . . . . . . . . 10 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> B e. C )
74	69, 70, 73	rspcdva 2860	. . . . . . . . 9 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` B ) e. B )
75		eqeq1 2195	. . . . . . . . . . 11 |- ( x = ( f ` B ) -> ( x = { (/) } <-> ( f ` B ) = { (/) } ) )
76	75	orbi1d 792	. . . . . . . . . 10 |- ( x = ( f ` B ) -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
77	76, 7	elrab2 2910	. . . . . . . . 9 |- ( ( f ` B ) e. B <-> ( ( f ` B ) e. { (/) , { (/) } } /\ ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
78	74, 77	sylib 122	. . . . . . . 8 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` B ) e. { (/) , { (/) } } /\ ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
79	78	simprd 114	. . . . . . 7 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` B ) = { (/) } \/ y = { (/) } ) )
80	79	adantr 276	. . . . . 6 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> ( ( f ` B ) = { (/) } \/ y = { (/) } ) )
81	64, 66, 80	mpjaodan 799	. . . . 5 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> ( y = { (/) } \/ -. y = { (/) } ) )
82		df-dc 836	. . . . 5 |- (DECID y = { (/) } <-> ( y = { (/) } \/ -. y = { (/) } ) )
83	81, 82	sylibr 134	. . . 4 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> DECID y = { (/) } )
84		simpr 110	. . . . . 6 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ y = { (/) } ) -> y = { (/) } )
85	84	orcd 734	. . . . 5 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ y = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
86	85, 82	sylibr 134	. . . 4 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ y = { (/) } ) -> DECID y = { (/) } )
87		fveq2 5529	. . . . . . . 8 |- ( z = A -> ( f ` z ) = ( f ` A ) )
88		id 19	. . . . . . . 8 |- ( z = A -> z = A )
89	87, 88	eleq12d 2259	. . . . . . 7 |- ( z = A -> ( ( f ` z ) e. z <-> ( f ` A ) e. A ) )
90	6	prid1 3712	. . . . . . . . 9 |- A e. { A , B }
91	90, 2	eleqtrri 2264	. . . . . . . 8 |- A e. C
92	91	a1i 9	. . . . . . 7 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> A e. C )
93	89, 70, 92	rspcdva 2860	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` A ) e. A )
94		eqeq1 2195	. . . . . . . 8 |- ( x = ( f ` A ) -> ( x = (/) <-> ( f ` A ) = (/) ) )
95	94	orbi1d 792	. . . . . . 7 |- ( x = ( f ` A ) -> ( ( x = (/) \/ y = { (/) } ) <-> ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
96	95, 3	elrab2 2910	. . . . . 6 |- ( ( f ` A ) e. A <-> ( ( f ` A ) e. { (/) , { (/) } } /\ ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
97	93, 96	sylib 122	. . . . 5 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` A ) e. { (/) , { (/) } } /\ ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
98	97	simprd 114	. . . 4 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` A ) = (/) \/ y = { (/) } ) )
99	83, 86, 98	mpjaodan 799	. . 3 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> DECID y = { (/) } )
100	44, 99	exlimddv 1909	. 2 |- ( (CHOICE /\ y C_ { (/) } ) -> DECID y = { (/) } )
101	100	exmid1dc 4214	1 |- (CHOICE -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 709  DECID wdc 835   = wceq 1363   E.wex 1502   e. wcel 2159   A.wral 2467   {crab 2471   _Vcvv 2751   C_ wss 3143   (/)c0 3436   {csn 3606   {cpr 3607  EXMIDwem 4208   Fn wfn 5225   ` cfv 5230  CHOICEwac 7221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-coll 4132  ax-sep 4135  ax-nul 4143  ax-pow 4188  ax-pr 4223  ax-un 4447

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-ral 2472  df-rex 2473  df-reu 2474  df-rab 2476  df-v 2753  df-sbc 2977  df-csb 3072  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-nul 3437  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-iun 3902  df-br 4018  df-opab 4079  df-mpt 4080  df-exmid 4209  df-id 4307  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-ac 7222

This theorem is referenced by:  exmidac  7225