Theorem exmidaclem 7422

Description: Lemma for exmidac 7423. 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 4279	. . . . . . . . 9 |- { (/) , { (/) } } e. _V
5	4	rabex 4234	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) } e. _V
6	3, 5	eqeltri 2304	. . . . . . 7 |- A e. _V
7		exmidaclem.b	. . . . . . . 8 |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }
8	4	rabex 4234	. . . . . . . 8 |- { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) } e. _V
9	7, 8	eqeltri 2304	. . . . . . 7 |- B e. _V
10		prexg 4301	. . . . . . 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 2304	. . . . 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 2324	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ z e. C ) -> z e. { A , B } )
16		elpri 3692	. . . . . 6 |- ( z e. { A , B } -> ( z = A \/ z = B ) )
17		0ex 4216	. . . . . . . . . . 11 |- (/) e. _V
18	17	prid1 3777	. . . . . . . . . 10 |- (/) e. { (/) , { (/) } }
19		eqid 2231	. . . . . . . . . . 11 |- (/) = (/)
20	19	orci 738	. . . . . . . . . 10 |- ( (/) = (/) \/ y = { (/) } )
21		eqeq1 2238	. . . . . . . . . . . 12 |- ( x = (/) -> ( x = (/) <-> (/) = (/) ) )
22	21	orbi1d 798	. . . . . . . . . . 11 |- ( x = (/) -> ( ( x = (/) \/ y = { (/) } ) <-> ( (/) = (/) \/ y = { (/) } ) ) )
23	22, 3	elrab2 2965	. . . . . . . . . 10 |- ( (/) e. A <-> ( (/) e. { (/) , { (/) } } /\ ( (/) = (/) \/ y = { (/) } ) ) )
24	18, 20, 23	mpbir2an 950	. . . . . . . . 9 |- (/) e. A
25		eleq2 2295	. . . . . . . . 9 |- ( z = A -> ( (/) e. z <-> (/) e. A ) )
26	24, 25	mpbiri 168	. . . . . . . 8 |- ( z = A -> (/) e. z )
27		elex2 2819	. . . . . . . 8 |- ( (/) e. z -> E. w w e. z )
28	26, 27	syl 14	. . . . . . 7 |- ( z = A -> E. w w e. z )
29		p0ex 4278	. . . . . . . . . . 11 |- { (/) } e. _V
30	29	prid2 3778	. . . . . . . . . 10 |- { (/) } e. { (/) , { (/) } }
31		eqid 2231	. . . . . . . . . . 11 |- { (/) } = { (/) }
32	31	orci 738	. . . . . . . . . 10 |- ( { (/) } = { (/) } \/ y = { (/) } )
33		eqeq1 2238	. . . . . . . . . . . 12 |- ( x = { (/) } -> ( x = { (/) } <-> { (/) } = { (/) } ) )
34	33	orbi1d 798	. . . . . . . . . . 11 |- ( x = { (/) } -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( { (/) } = { (/) } \/ y = { (/) } ) ) )
35	34, 7	elrab2 2965	. . . . . . . . . 10 |- ( { (/) } e. B <-> ( { (/) } e. { (/) , { (/) } } /\ ( { (/) } = { (/) } \/ y = { (/) } ) ) )
36	30, 32, 35	mpbir2an 950	. . . . . . . . 9 |- { (/) } e. B
37		eleq2 2295	. . . . . . . . 9 |- ( z = B -> ( { (/) } e. z <-> { (/) } e. B ) )
38	36, 37	mpbiri 168	. . . . . . . 8 |- ( z = B -> { (/) } e. z )
39		elex2 2819	. . . . . . . 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 723	. . . . . 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 2605	. . . 4 |- ( (CHOICE /\ y C_ { (/) } ) -> A. z e. C E. w w e. z )
44	1, 13, 43	acfun 7421	. . 3 |- ( (CHOICE /\ y C_ { (/) } ) -> E. f ( f Fn C /\ A. z e. C ( f ` z ) e. z ) )
45		0nep0 4255	. . . . . . . . . 10 |- (/) =/= { (/) }
46	45	neii 2404	. . . . . . . . 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 2246	. . . . . . . . 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 681	. . . . . . . 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 718	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = (/) \/ y = { (/) } ) )
52	51	ralrimivw 2606	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = (/) \/ y = { (/) } ) )
53		rabid2 2710	. . . . . . . . . . . 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 2282	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = A )
56		olc 718	. . . . . . . . . . . . 13 |- ( y = { (/) } -> ( x = { (/) } \/ y = { (/) } ) )
57	56	ralrimivw 2606	. . . . . . . . . . . 12 |- ( y = { (/) } -> A. x e. { (/) , { (/) } } ( x = { (/) } \/ y = { (/) } ) )
58		rabid2 2710	. . . . . . . . . . . 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 2282	. . . . . . . . . 10 |- ( y = { (/) } -> { (/) , { (/) } } = B )
61	55, 60	eqtr3d 2266	. . . . . . . . 9 |- ( y = { (/) } -> A = B )
62	61	fveq2d 5643	. . . . . . . 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 741	. . . . . 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 740	. . . . . 6 |- ( ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) /\ y = { (/) } ) -> ( y = { (/) } \/ -. y = { (/) } ) )
67		fveq2 5639	. . . . . . . . . . 11 |- ( z = B -> ( f ` z ) = ( f ` B ) )
68		id 19	. . . . . . . . . . 11 |- ( z = B -> z = B )
69	67, 68	eleq12d 2302	. . . . . . . . . 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 3778	. . . . . . . . . . . 12 |- B e. { A , B }
72	71, 2	eleqtrri 2307	. . . . . . . . . . 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 2915	. . . . . . . . 9 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` B ) e. B )
75		eqeq1 2238	. . . . . . . . . . 11 |- ( x = ( f ` B ) -> ( x = { (/) } <-> ( f ` B ) = { (/) } ) )
76	75	orbi1d 798	. . . . . . . . . 10 |- ( x = ( f ` B ) -> ( ( x = { (/) } \/ y = { (/) } ) <-> ( ( f ` B ) = { (/) } \/ y = { (/) } ) ) )
77	76, 7	elrab2 2965	. . . . . . . . 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 805	. . . . 5 |- ( ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) /\ ( f ` A ) = (/) ) -> ( y = { (/) } \/ -. y = { (/) } ) )
82		df-dc 842	. . . . 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 740	. . . . 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 5639	. . . . . . . 8 |- ( z = A -> ( f ` z ) = ( f ` A ) )
88		id 19	. . . . . . . 8 |- ( z = A -> z = A )
89	87, 88	eleq12d 2302	. . . . . . 7 |- ( z = A -> ( ( f ` z ) e. z <-> ( f ` A ) e. A ) )
90	6	prid1 3777	. . . . . . . . 9 |- A e. { A , B }
91	90, 2	eleqtrri 2307	. . . . . . . 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 2915	. . . . . 6 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> ( f ` A ) e. A )
94		eqeq1 2238	. . . . . . . 8 |- ( x = ( f ` A ) -> ( x = (/) <-> ( f ` A ) = (/) ) )
95	94	orbi1d 798	. . . . . . 7 |- ( x = ( f ` A ) -> ( ( x = (/) \/ y = { (/) } ) <-> ( ( f ` A ) = (/) \/ y = { (/) } ) ) )
96	95, 3	elrab2 2965	. . . . . 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 805	. . 3 |- ( ( (CHOICE /\ y C_ { (/) } ) /\ ( f Fn C /\ A. z e. C ( f ` z ) e. z ) ) -> DECID y = { (/) } )
100	44, 99	exlimddv 1947	. 2 |- ( (CHOICE /\ y C_ { (/) } ) -> DECID y = { (/) } )
101	100	exmid1dc 4290	1 |- (CHOICE -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 715  DECID wdc 841   = wceq 1397   E.wex 1540   e. wcel 2202   A.wral 2510   {crab 2514   _Vcvv 2802   C_ wss 3200   (/)c0 3494   {csn 3669   {cpr 3670  EXMIDwem 4284   Fn wfn 5321   ` cfv 5326  CHOICEwac 7419

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530

This theorem depends on definitions:  df-bi 117  df-dc 842  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-exmid 4285  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-ac 7420

This theorem is referenced by:  exmidac  7423