Theorem exmidaclem 7515

Description: Lemma for exmidac 7516. 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 4302	. . . . . . . . 9 |- { (/) , { (/) } } e. _V
5	4	rabex 4256	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } e. _V
6	3, 5	eqeltri 2305	. . . . . . 7 |- A e. _V
7		exmidaclem.b	. . . . . . . 8 |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }
8	4	rabex 4256	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } e. _V
9	7, 8	eqeltri 2305	. . . . . . 7 |- B e. _V
10		prexg 4325	. . . . . . 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 2305	. . . . 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 2325	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> z e. { A , B } )
16		elpri 3712	. . . . . 6 |- ( z e. { A , B } -> ( z = A \/ z = B ) )
17		0ex 4237	. . . . . . . . . . 11 |- (/) e. _V
18	17	prid1 3797	. . . . . . . . . 10 |- (/) e. { (/) , { (/) } }
19		eqid 2232	. . . . . . . . . . 11 |- (/) = (/)
20	19	orci 739	. . . . . . . . . 10 |- ( (/) = (/) \/ y = { (/) } )
21		eqeq1 2239	. . . . . . . . . . . 12 |- ( x = (/) -> ( x = (/) <-> (/) = (/) ) )
22	21	orbi1d 799	. . . . . . . . . . 11 |- ( x = (/) -> ( ( x = (/) \/ y = { (/) } ) <-> ( (/) = (/) \/ y = { (/) } ) ) )
23	22, 3	elrab2 2976	. . . . . . . . . 10 |- ( (/) e. A <-> ( (/) e. { (/) , { (/) } } /\ ( (/) = (/) \/ y = { (/) } ) ) )
24	18, 20, 23	mpbir2an 951	. . . . . . . . 9 |- (/) e. A
25		eleq2 2296	. . . . . . . . 9 |- ( z = A -> ( (/) e. z <-> (/) e. A ) )
26	24, 25	mpbiri 168	. . . . . . . 8 |- ( z = A -> (/) e. z )
27		elex2 2830	. . . . . . . 8 |- ( (/) e. z -> E. w w e. z )
28	26, 27	syl 14	. . . . . . 7 |- ( z = A -> E. w w e. z )
29		p0ex 4301	. . . . . . . . . . 11 |- { (/) } e. _V
30	29	prid2 3798	. . . . . . . . . 10 |- { (/) } e. { (/) , { (/) } }
31		eqid 2232	. . . . . . . . . . 11 |- { (/) } = { (/) }
32	31	orci 739	. . . . . . . . . 10 |- ( { (/) } = { (/) } \/ y = { (/) } )
33		eqeq1 2239	. . . . . . . . . . . 12 |- ( x = { (/) } -> ( x = { (/) } <-> { (/) } = { (/) } ) )
34	33	orbi1d 799	. . . . . . . . . . 11 |- ( x = { (/) } -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( { (/) } = { (/) } \/ y = { (/) } ) ) )
35	34, 7	elrab2 2976	. . . . . . . . . 10 |- ( { (/) } e. B <-> ( { (/) } e. { (/) , { (/) } } /\ ( { (/) } = { (/) } \/ y = { (/) } ) ) )
36	30, 32, 35	mpbir2an 951	. . . . . . . . 9 |- { (/) } e. B
37		eleq2 2296	. . . . . . . . 9 |- ( z = B -> ( { (/) } e. z <-> { (/) } e. B ) )
38	36, 37	mpbiri 168	. . . . . . . 8 |- ( z = B -> { (/) } e. z )
39		elex2 2830	. . . . . . . 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 724	. . . . . 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 2615	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> A. z e. C E. w w e. z )
44	1, 13, 43	acfun 7514	. . 3 |- ( (CHOICE /\ y C_ { (/) } ) -> E. f ( f Fn C /\ A. z e. C ( f ` z ) e. z ) )
45		0nep0 4278	. . . . . . . . . 10 |- (/) =/= { (/) }
46	45	neii 2414	. . . . . . . . 9 |- -. (/) = { (/) }
47		simplr 529	. . . . . . . . . 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 2247	. . . . . . . . 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 682	. . . . . . . 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 719	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = (/) \/ y = { (/) } ) )
52	51	ralrimivw 2616	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = (/) \/ y = { (/) } ) )
53		rabid2 2721	. . . . . . . . . . . 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 2283	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = A )
56		olc 719	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = { (/) } \/ y = { (/) } ) )
57	56	ralrimivw 2616	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = { (/) } \/ y = { (/) } ) )
58		rabid2 2721	. . . . . . . . . . . 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 2283	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = B )
61	55, 60	eqtr3d 2267	. . . . . . . . 9 |- ( y = { (/) } -> A = B )
62	61	fveq2d 5674	. . . . . . . 8 |- ( y = { (/) } -> ( f ` A ) = ( f ` B ) )
63	50, 62	nsyl 633	. . . . . . 7 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ ( f ` B ) = { (/) } ) -> -. y = { (/) } )
64	63	olcd 742	. . . . . 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 741	. . . . . 6 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ y = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
67		fveq2 5670	. . . . . . . . . . 11 |- ( z = B -> ( f ` z ) = ( f ` B ) )
68		id 19	. . . . . . . . . . 11 |- ( z = B -> z = B )
69	67, 68	eleq12d 2303	. . . . . . . . . 10 |- ( z = B -> ( ( f ` z ) e. z <-> ( f ` B ) e. B ) )
70		simprr 533	. . . . . . . . . 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 3798	. . . . . . . . . . . 12 |- B e. { A , B }
72	71, 2	eleqtrri 2308	. . . . . . . . . . 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 2926	. . . . . . . . 9 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` B ) e. B )
75		eqeq1 2239	. . . . . . . . . . 11 |- ( x = ( f ` B ) -> ( x = { (/) } <-> ( f ` B ) = { (/) } ) )
76	75	orbi1d 799	. . . . . . . . . 10 |- ( x = ( f ` B ) -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
77	76, 7	elrab2 2976	. . . . . . . . 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 806	. . . . 5 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> ( y = { (/) } \/ -. y = { (/) } ) )
82		df-dc 843	. . . . 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 741	. . . . 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 5670	. . . . . . . 8 |- ( z = A -> ( f ` z ) = ( f ` A ) )
88		id 19	. . . . . . . 8 |- ( z = A -> z = A )
89	87, 88	eleq12d 2303	. . . . . . 7 |- ( z = A -> ( ( f ` z ) e. z <-> ( f ` A ) e. A ) )
90	6	prid1 3797	. . . . . . . . 9 |- A e. { A , B }
91	90, 2	eleqtrri 2308	. . . . . . . 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 2926	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` A ) e. A )
94		eqeq1 2239	. . . . . . . 8 |- ( x = ( f ` A ) -> ( x = (/) <-> ( f ` A ) = (/) ) )
95	94	orbi1d 799	. . . . . . 7 |- ( x = ( f ` A ) -> ( ( x = (/) \/ y = { (/) } ) <-> ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
96	95, 3	elrab2 2976	. . . . . 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 806	. . 3 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> DECID y = { (/) } )
100	44, 99	exlimddv 1948	. 2 |- ( (CHOICE /\ y C_ { (/) } ) -> DECID y = { (/) } )
101	100	exmid1dc 4313	1 |- (CHOICE -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 716  DECID wdc 842   = wceq 1398   E.wex 1541   e. wcel 2203   A.wral 2520   {crab 2524   _Vcvv 2813   C_ wss 3211   (/)c0 3508   {csn 3689   {cpr 3690  EXMIDwem 4307   Fn wfn 5347   ` cfv 5352  CHOICEwac 7512

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4225  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-iun 3993  df-br 4110  df-opab 4172  df-mpt 4173  df-exmid 4308  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-fv 5360  df-ac 7513

This theorem is referenced by:  exmidac  7516