Metamath Proof Explorer

Theorem aciunf1

Description: Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020)

Ref Expression
Hypotheses aciunf1.0 
|- ( ph -> A e. V )
aciunf1.1 
|- ( ( ph /\ j e. A ) -> B e. W )
Assertion aciunf1 
|- ( ph -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. k e. U_ j e. A B ( 2nd ` ( f ` k ) ) = k ) )

Proof

Step Hyp Ref Expression
1 aciunf1.0 
 |-  ( ph -> A e. V )
2 aciunf1.1 
 |-  ( ( ph /\ j e. A ) -> B e. W )
3 ssrab2 
 |-  { j e. A | B =/= (/) } C_ A
4 ssexg 
 |-  ( ( { j e. A | B =/= (/) } C_ A /\ A e. V ) -> { j e. A | B =/= (/) } e. _V )
5 3 1 4 sylancr 
 |-  ( ph -> { j e. A | B =/= (/) } e. _V )
6 rabid 
 |-  ( j e. { j e. A | B =/= (/) } <-> ( j e. A /\ B =/= (/) ) )
7 6 bilani 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> ( j e. A /\ B =/= (/) ) )
8 7 simprd 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> B =/= (/) )
9 nfrab1 
 |-  F/_ j { j e. A | B =/= (/) }
10 7 simpld 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> j e. A )
11 10 2 syldan 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> B e. W )
12 5 8 9 11 aciunf1lem 
 |-  ( ph -> E. f ( f : U_ j e. { j e. A | B =/= (/) } B -1-1-> U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) /\ A. k e. U_ j e. { j e. A | B =/= (/) } B ( 2nd ` ( f ` k ) ) = k ) )
13 eqidd 
 |-  ( ph -> f = f )
14 nfv 
 |-  F/ j ph
15 nfcv 
 |-  F/_ j A
16 nfrab1 
 |-  F/_ j { j e. A | B = (/) }
17 15 16 nfdif 
 |-  F/_ j ( A \ { j e. A | B = (/) } )
18 difrab 
 |-  ( { j e. A | T. } \ { j e. A | B = (/) } ) = { j e. A | ( T. /\ -. B = (/) ) }
19 15 rabtru 
 |-  { j e. A | T. } = A
20 19 difeq1i 
 |-  ( { j e. A | T. } \ { j e. A | B = (/) } ) = ( A \ { j e. A | B = (/) } )
21 truan 
 |-  ( ( T. /\ -. B = (/) ) <-> -. B = (/) )
22 df-ne 
 |-  ( B =/= (/) <-> -. B = (/) )
23 21 22 bitr4i 
 |-  ( ( T. /\ -. B = (/) ) <-> B =/= (/) )
24 23 rabbii 
 |-  { j e. A | ( T. /\ -. B = (/) ) } = { j e. A | B =/= (/) }
25 18 20 24 3eqtr3i 
 |-  ( A \ { j e. A | B = (/) } ) = { j e. A | B =/= (/) }
26 25 a1i 
 |-  ( ph -> ( A \ { j e. A | B = (/) } ) = { j e. A | B =/= (/) } )
27 eqidd 
 |-  ( ph -> B = B )
28 14 17 9 26 27 iuneq12df 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) B = U_ j e. { j e. A | B =/= (/) } B )
29 rabid 
 |-  ( j e. { j e. A | B = (/) } <-> ( j e. A /\ B = (/) ) )
30 29 bilani 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> ( j e. A /\ B = (/) ) )
31 30 simprd 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> B = (/) )
32 31 ralrimiva 
 |-  ( ph -> A. j e. { j e. A | B = (/) } B = (/) )
33 16 iunxdif3 
 |-  ( A. j e. { j e. A | B = (/) } B = (/) -> U_ j e. ( A \ { j e. A | B = (/) } ) B = U_ j e. A B )
34 32 33 syl 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) B = U_ j e. A B )
35 28 34 eqtr3d 
 |-  ( ph -> U_ j e. { j e. A | B =/= (/) } B = U_ j e. A B )
36 eqidd 
 |-  ( ph -> ( { j } X. B ) = ( { j } X. B ) )
37 14 17 9 26 36 iuneq12df 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) ( { j } X. B ) = U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) )
38 31 xpeq2d 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> ( { j } X. B ) = ( { j } X. (/) ) )
39 xp0 
 |-  ( { j } X. (/) ) = (/)
40 38 39 eqtrdi 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> ( { j } X. B ) = (/) )
41 40 ralrimiva 
 |-  ( ph -> A. j e. { j e. A | B = (/) } ( { j } X. B ) = (/) )
42 16 iunxdif3 
 |-  ( A. j e. { j e. A | B = (/) } ( { j } X. B ) = (/) -> U_ j e. ( A \ { j e. A | B = (/) } ) ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
43 41 42 syl 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
44 37 43 eqtr3d 
 |-  ( ph -> U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
45 13 35 44 f1eq123d 
 |-  ( ph -> ( f : U_ j e. { j e. A | B =/= (/) } B -1-1-> U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) <-> f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) ) )
46 35 raleqdv 
 |-  ( ph -> ( A. k e. U_ j e. { j e. A | B =/= (/) } B ( 2nd ` ( f ` k ) ) = k <-> A. k e. U_ j e. A B ( 2nd ` ( f ` k ) ) = k ) )
47 45 46 anbi12d 
 |-  ( ph -> ( ( f : U_ j e. { j e. A | B =/= (/) } B -1-1-> U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) /\ A. k e. U_ j e. { j e. A | B =/= (/) } B ( 2nd ` ( f ` k ) ) = k ) <-> ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. k e. U_ j e. A B ( 2nd ` ( f ` k ) ) = k ) ) )
48 47 exbidv 
 |-  ( ph -> ( E. f ( f : U_ j e. { j e. A | B =/= (/) } B -1-1-> U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) /\ A. k e. U_ j e. { j e. A | B =/= (/) } B ( 2nd ` ( f ` k ) ) = k ) <-> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. k e. U_ j e. A B ( 2nd ` ( f ` k ) ) = k ) ) )
49 12 48 mpbid 
 |-  ( ph -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. k e. U_ j e. A B ( 2nd ` ( f ` k ) ) = k ) )