Theorem exmidaclem 7122

Description: Lemma for exmidac 7123. 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 108	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> CHOICE )
2		exmidaclem.c	. . . . . 6 |- C = { A , B }
3		exmidaclem.a	. . . . . . . 8 |- A = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) }
4		pp0ex 4145	. . . . . . . . 9 |- { (/) , { (/) } } e. _V
5	4	rabex 4104	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } e. _V
6	3, 5	eqeltri 2227	. . . . . . 7 |- A e. _V
7		exmidaclem.b	. . . . . . . 8 |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }
8	4	rabex 4104	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } e. _V
9	7, 8	eqeltri 2227	. . . . . . 7 |- B e. _V
10		prexg 4166	. . . . . . 7 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
11	6, 9, 10	mp2an 423	. . . . . 6 |- { A , B } e. _V
12	2, 11	eqeltri 2227	. . . . 5 |- C e. _V
13	12	a1i 9	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> C e. _V )
14		simpr 109	. . . . . . 7 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> z e. C )
15	14, 2	eleqtrdi 2247	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> z e. { A , B } )
16		elpri 3579	. . . . . 6 |- ( z e. { A , B } -> ( z = A \/ z = B ) )
17		0ex 4087	. . . . . . . . . . 11 |- (/) e. _V
18	17	prid1 3661	. . . . . . . . . 10 |- (/) e. { (/) , { (/) } }
19		eqid 2154	. . . . . . . . . . 11 |- (/) = (/)
20	19	orci 721	. . . . . . . . . 10 |- ( (/) = (/) \/ y = { (/) } )
21		eqeq1 2161	. . . . . . . . . . . 12 |- ( x = (/) -> ( x = (/) <-> (/) = (/) ) )
22	21	orbi1d 781	. . . . . . . . . . 11 |- ( x = (/) -> ( ( x = (/) \/ y = { (/) } ) <-> ( (/) = (/) \/ y = { (/) } ) ) )
23	22, 3	elrab2 2867	. . . . . . . . . 10 |- ( (/) e. A <-> ( (/) e. { (/) , { (/) } } /\ ( (/) = (/) \/ y = { (/) } ) ) )
24	18, 20, 23	mpbir2an 927	. . . . . . . . 9 |- (/) e. A
25		eleq2 2218	. . . . . . . . 9 |- ( z = A -> ( (/) e. z <-> (/) e. A ) )
26	24, 25	mpbiri 167	. . . . . . . 8 |- ( z = A -> (/) e. z )
27		elex2 2725	. . . . . . . 8 |- ( (/) e. z -> E. w w e. z )
28	26, 27	syl 14	. . . . . . 7 |- ( z = A -> E. w w e. z )
29		p0ex 4144	. . . . . . . . . . 11 |- { (/) } e. _V
30	29	prid2 3662	. . . . . . . . . 10 |- { (/) } e. { (/) , { (/) } }
31		eqid 2154	. . . . . . . . . . 11 |- { (/) } = { (/) }
32	31	orci 721	. . . . . . . . . 10 |- ( { (/) } = { (/) } \/ y = { (/) } )
33		eqeq1 2161	. . . . . . . . . . . 12 |- ( x = { (/) } -> ( x = { (/) } <-> { (/) } = { (/) } ) )
34	33	orbi1d 781	. . . . . . . . . . 11 |- ( x = { (/) } -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( { (/) } = { (/) } \/ y = { (/) } ) ) )
35	34, 7	elrab2 2867	. . . . . . . . . 10 |- ( { (/) } e. B <-> ( { (/) } e. { (/) , { (/) } } /\ ( { (/) } = { (/) } \/ y = { (/) } ) ) )
36	30, 32, 35	mpbir2an 927	. . . . . . . . 9 |- { (/) } e. B
37		eleq2 2218	. . . . . . . . 9 |- ( z = B -> ( { (/) } e. z <-> { (/) } e. B ) )
38	36, 37	mpbiri 167	. . . . . . . 8 |- ( z = B -> { (/) } e. z )
39		elex2 2725	. . . . . . . 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 706	. . . . . 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 2527	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> A. z e. C E. w w e. z )
44	1, 13, 43	acfun 7121	. . 3 |- ( (CHOICE /\ y C_ { (/) } ) -> E. f ( f Fn C /\ A. z e. C ( f ` z ) e. z ) )
45		0nep0 4121	. . . . . . . . . 10 |- (/) =/= { (/) }
46	45	neii 2326	. . . . . . . . 9 |- -. (/) = { (/) }
47		simplr 520	. . . . . . . . . 10 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> ( f ` A ) = (/) )
48		simpr 109	. . . . . . . . . 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 2169	. . . . . . . . 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 665	. . . . . . . 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 701	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = (/) \/ y = { (/) } ) )
52	51	ralrimivw 2528	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = (/) \/ y = { (/) } ) )
53		rabid2 2630	. . . . . . . . . . . 12 |- ( { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } <-> A. x e. { (/) , { (/) } } ( x = (/) \/ y = { (/) } ) )
54	52, 53	sylibr 133	. . . . . . . . . . 11 |- ( y = { (/) } -> { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } )
55	54, 3	eqtr4di 2205	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = A )
56		olc 701	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = { (/) } \/ y = { (/) } ) )
57	56	ralrimivw 2528	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = { (/) } \/ y = { (/) } ) )
58		rabid2 2630	. . . . . . . . . . . 12 |- ( { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } <-> A. x e. { (/) , { (/) } } ( x = { (/) } \/ y = { (/) } ) )
59	57, 58	sylibr 133	. . . . . . . . . . 11 |- ( y = { (/) } -> { (/) , { (/) } } = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } )
60	59, 7	eqtr4di 2205	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = B )
61	55, 60	eqtr3d 2189	. . . . . . . . 9 |- ( y = { (/) } -> A = B )
62	61	fveq2d 5465	. . . . . . . 8 |- ( y = { (/) } -> ( f ` A ) = ( f ` B ) )
63	50, 62	nsyl 618	. . . . . . 7 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> -. y = { (/) } )
64	63	olcd 724	. . . . . 6 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
65		simpr 109	. . . . . . 7 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ y = { (/) } ) -> y = { (/) } )
66	65	orcd 723	. . . . . 6 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ y = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
67		fveq2 5461	. . . . . . . . . . 11 |- ( z = B -> ( f ` z ) = ( f ` B ) )
68		id 19	. . . . . . . . . . 11 |- ( z = B -> z = B )
69	67, 68	eleq12d 2225	. . . . . . . . . 10 |- ( z = B -> ( ( f ` z ) e. z <-> ( f ` B ) e. B ) )
70		simprr 522	. . . . . . . . . 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 3662	. . . . . . . . . . . 12 |- B e. { A , B }
72	71, 2	eleqtrri 2230	. . . . . . . . . . 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 2818	. . . . . . . . 9 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` B ) e. B )
75		eqeq1 2161	. . . . . . . . . . 11 |- ( x = ( f ` B ) -> ( x = { (/) } <-> ( f ` B ) = { (/) } ) )
76	75	orbi1d 781	. . . . . . . . . 10 |- ( x = ( f ` B ) -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
77	76, 7	elrab2 2867	. . . . . . . . 9 |- ( ( f ` B ) e. B <-> ( ( f ` B ) e. { (/) , { (/) } } /\ ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
78	74, 77	sylib 121	. . . . . . . 8 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` B ) e. { (/) , { (/) } } /\ ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
79	78	simprd 113	. . . . . . 7 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` B ) = { (/) } \/ y = { (/) } ) )
80	79	adantr 274	. . . . . 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 788	. . . . 5 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> ( y = { (/) } \/ -. y = { (/) } ) )
82		df-dc 821	. . . . 5 |- (DECID y = { (/) } <-> ( y = { (/) } \/ -. y = { (/) } ) )
83	81, 82	sylibr 133	. . . 4 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> DECID y = { (/) } )
84		simpr 109	. . . . . 6 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ y = { (/) } ) -> y = { (/) } )
85	84	orcd 723	. . . . 5 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ y = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
86	85, 82	sylibr 133	. . . 4 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ y = { (/) } ) -> DECID y = { (/) } )
87		fveq2 5461	. . . . . . . 8 |- ( z = A -> ( f ` z ) = ( f ` A ) )
88		id 19	. . . . . . . 8 |- ( z = A -> z = A )
89	87, 88	eleq12d 2225	. . . . . . 7 |- ( z = A -> ( ( f ` z ) e. z <-> ( f ` A ) e. A ) )
90	6	prid1 3661	. . . . . . . . 9 |- A e. { A , B }
91	90, 2	eleqtrri 2230	. . . . . . . 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 2818	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` A ) e. A )
94		eqeq1 2161	. . . . . . . 8 |- ( x = ( f ` A ) -> ( x = (/) <-> ( f ` A ) = (/) ) )
95	94	orbi1d 781	. . . . . . 7 |- ( x = ( f ` A ) -> ( ( x = (/) \/ y = { (/) } ) <-> ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
96	95, 3	elrab2 2867	. . . . . 6 |- ( ( f ` A ) e. A <-> ( ( f ` A ) e. { (/) , { (/) } } /\ ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
97	93, 96	sylib 121	. . . . 5 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` A ) e. { (/) , { (/) } } /\ ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
98	97	simprd 113	. . . 4 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( ( f ` A ) = (/) \/ y = { (/) } ) )
99	83, 86, 98	mpjaodan 788	. . 3 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> DECID y = { (/) } )
100	44, 99	exlimddv 1875	. 2 |- ( (CHOICE /\ y C_ { (/) } ) -> DECID y = { (/) } )
101	100	exmid1dc 4156	1 |- (CHOICE -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 698  DECID wdc 820   = wceq 1332   E.wex 1469   e. wcel 2125   A.wral 2432   {crab 2436   _Vcvv 2709   C_ wss 3098   (/)c0 3390   {csn 3556   {cpr 3557  EXMIDwem 4150   Fn wfn 5158   ` cfv 5163  CHOICEwac 7119

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388

This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-ral 2437  df-rex 2438  df-reu 2439  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-exmid 4151  df-id 4248  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-ac 7120

This theorem is referenced by:  exmidac  7123