Theorem exmidaclem 7320

Description: Lemma for exmidac 7321. 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 4233	. . . . . . . . 9 |- { (/) , { (/) } } e. _V
5	4	rabex 4188	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } e. _V
6	3, 5	eqeltri 2278	. . . . . . 7 |- A e. _V
7		exmidaclem.b	. . . . . . . 8 |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }
8	4	rabex 4188	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } e. _V
9	7, 8	eqeltri 2278	. . . . . . 7 |- B e. _V
10		prexg 4255	. . . . . . 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 2278	. . . . 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 2298	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> z e. { A , B } )
16		elpri 3656	. . . . . 6 |- ( z e. { A , B } -> ( z = A \/ z = B ) )
17		0ex 4171	. . . . . . . . . . 11 |- (/) e. _V
18	17	prid1 3739	. . . . . . . . . 10 |- (/) e. { (/) , { (/) } }
19		eqid 2205	. . . . . . . . . . 11 |- (/) = (/)
20	19	orci 733	. . . . . . . . . 10 |- ( (/) = (/) \/ y = { (/) } )
21		eqeq1 2212	. . . . . . . . . . . 12 |- ( x = (/) -> ( x = (/) <-> (/) = (/) ) )
22	21	orbi1d 793	. . . . . . . . . . 11 |- ( x = (/) -> ( ( x = (/) \/ y = { (/) } ) <-> ( (/) = (/) \/ y = { (/) } ) ) )
23	22, 3	elrab2 2932	. . . . . . . . . 10 |- ( (/) e. A <-> ( (/) e. { (/) , { (/) } } /\ ( (/) = (/) \/ y = { (/) } ) ) )
24	18, 20, 23	mpbir2an 945	. . . . . . . . 9 |- (/) e. A
25		eleq2 2269	. . . . . . . . 9 |- ( z = A -> ( (/) e. z <-> (/) e. A ) )
26	24, 25	mpbiri 168	. . . . . . . 8 |- ( z = A -> (/) e. z )
27		elex2 2788	. . . . . . . 8 |- ( (/) e. z -> E. w w e. z )
28	26, 27	syl 14	. . . . . . 7 |- ( z = A -> E. w w e. z )
29		p0ex 4232	. . . . . . . . . . 11 |- { (/) } e. _V
30	29	prid2 3740	. . . . . . . . . 10 |- { (/) } e. { (/) , { (/) } }
31		eqid 2205	. . . . . . . . . . 11 |- { (/) } = { (/) }
32	31	orci 733	. . . . . . . . . 10 |- ( { (/) } = { (/) } \/ y = { (/) } )
33		eqeq1 2212	. . . . . . . . . . . 12 |- ( x = { (/) } -> ( x = { (/) } <-> { (/) } = { (/) } ) )
34	33	orbi1d 793	. . . . . . . . . . 11 |- ( x = { (/) } -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( { (/) } = { (/) } \/ y = { (/) } ) ) )
35	34, 7	elrab2 2932	. . . . . . . . . 10 |- ( { (/) } e. B <-> ( { (/) } e. { (/) , { (/) } } /\ ( { (/) } = { (/) } \/ y = { (/) } ) ) )
36	30, 32, 35	mpbir2an 945	. . . . . . . . 9 |- { (/) } e. B
37		eleq2 2269	. . . . . . . . 9 |- ( z = B -> ( { (/) } e. z <-> { (/) } e. B ) )
38	36, 37	mpbiri 168	. . . . . . . 8 |- ( z = B -> { (/) } e. z )
39		elex2 2788	. . . . . . . 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 718	. . . . . 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 2579	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> A. z e. C E. w w e. z )
44	1, 13, 43	acfun 7319	. . 3 |- ( (CHOICE /\ y C_ { (/) } ) -> E. f ( f Fn C /\ A. z e. C ( f ` z ) e. z ) )
45		0nep0 4209	. . . . . . . . . 10 |- (/) =/= { (/) }
46	45	neii 2378	. . . . . . . . 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 2220	. . . . . . . . 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 677	. . . . . . . 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 713	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = (/) \/ y = { (/) } ) )
52	51	ralrimivw 2580	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = (/) \/ y = { (/) } ) )
53		rabid2 2683	. . . . . . . . . . . 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 2256	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = A )
56		olc 713	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = { (/) } \/ y = { (/) } ) )
57	56	ralrimivw 2580	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = { (/) } \/ y = { (/) } ) )
58		rabid2 2683	. . . . . . . . . . . 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 2256	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = B )
61	55, 60	eqtr3d 2240	. . . . . . . . 9 |- ( y = { (/) } -> A = B )
62	61	fveq2d 5580	. . . . . . . 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 736	. . . . . 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 735	. . . . . 6 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ y = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
67		fveq2 5576	. . . . . . . . . . 11 |- ( z = B -> ( f ` z ) = ( f ` B ) )
68		id 19	. . . . . . . . . . 11 |- ( z = B -> z = B )
69	67, 68	eleq12d 2276	. . . . . . . . . 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 3740	. . . . . . . . . . . 12 |- B e. { A , B }
72	71, 2	eleqtrri 2281	. . . . . . . . . . 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 2882	. . . . . . . . 9 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` B ) e. B )
75		eqeq1 2212	. . . . . . . . . . 11 |- ( x = ( f ` B ) -> ( x = { (/) } <-> ( f ` B ) = { (/) } ) )
76	75	orbi1d 793	. . . . . . . . . 10 |- ( x = ( f ` B ) -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
77	76, 7	elrab2 2932	. . . . . . . . 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 800	. . . . 5 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> ( y = { (/) } \/ -. y = { (/) } ) )
82		df-dc 837	. . . . 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 735	. . . . 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 5576	. . . . . . . 8 |- ( z = A -> ( f ` z ) = ( f ` A ) )
88		id 19	. . . . . . . 8 |- ( z = A -> z = A )
89	87, 88	eleq12d 2276	. . . . . . 7 |- ( z = A -> ( ( f ` z ) e. z <-> ( f ` A ) e. A ) )
90	6	prid1 3739	. . . . . . . . 9 |- A e. { A , B }
91	90, 2	eleqtrri 2281	. . . . . . . 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 2882	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` A ) e. A )
94		eqeq1 2212	. . . . . . . 8 |- ( x = ( f ` A ) -> ( x = (/) <-> ( f ` A ) = (/) ) )
95	94	orbi1d 793	. . . . . . 7 |- ( x = ( f ` A ) -> ( ( x = (/) \/ y = { (/) } ) <-> ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
96	95, 3	elrab2 2932	. . . . . 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 800	. . 3 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> DECID y = { (/) } )
100	44, 99	exlimddv 1922	. 2 |- ( (CHOICE /\ y C_ { (/) } ) -> DECID y = { (/) } )
101	100	exmid1dc 4244	1 |- (CHOICE -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 710  DECID wdc 836   = wceq 1373   E.wex 1515   e. wcel 2176   A.wral 2484   {crab 2488   _Vcvv 2772   C_ wss 3166   (/)c0 3460   {csn 3633   {cpr 3634  EXMIDwem 4238   Fn wfn 5266   ` cfv 5271  CHOICEwac 7317

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-coll 4159  ax-sep 4162  ax-nul 4170  ax-pow 4218  ax-pr 4253  ax-un 4480

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-ral 2489  df-rex 2490  df-reu 2491  df-rab 2493  df-v 2774  df-sbc 2999  df-csb 3094  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3461  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-iun 3929  df-br 4045  df-opab 4106  df-mpt 4107  df-exmid 4239  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ac 7318

This theorem is referenced by:  exmidac  7321