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 biimpi 
 |-  ( j e. { j e. A | B =/= (/) } -> ( j e. A /\ B =/= (/) ) )
8 7 adantl 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> ( j e. A /\ B =/= (/) ) )
9 8 simprd 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> B =/= (/) )
10 nfrab1 
 |-  F/_ j { j e. A | B =/= (/) }
11 8 simpld 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> j e. A )
12 11 2 syldan 
 |-  ( ( ph /\ j e. { j e. A | B =/= (/) } ) -> B e. W )
13 5 9 10 12 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 ) )
14 eqidd 
 |-  ( ph -> f = f )
15 nfv 
 |-  F/ j ph
16 nfcv 
 |-  F/_ j A
17 nfrab1 
 |-  F/_ j { j e. A | B = (/) }
18 16 17 nfdif 
 |-  F/_ j ( A \ { j e. A | B = (/) } )
19 difrab 
 |-  ( { j e. A | T. } \ { j e. A | B = (/) } ) = { j e. A | ( T. /\ -. B = (/) ) }
20 16 rabtru 
 |-  { j e. A | T. } = A
21 20 difeq1i 
 |-  ( { j e. A | T. } \ { j e. A | B = (/) } ) = ( A \ { j e. A | B = (/) } )
22 truan 
 |-  ( ( T. /\ -. B = (/) ) <-> -. B = (/) )
23 df-ne 
 |-  ( B =/= (/) <-> -. B = (/) )
24 22 23 bitr4i 
 |-  ( ( T. /\ -. B = (/) ) <-> B =/= (/) )
25 24 rabbii 
 |-  { j e. A | ( T. /\ -. B = (/) ) } = { j e. A | B =/= (/) }
26 19 21 25 3eqtr3i 
 |-  ( A \ { j e. A | B = (/) } ) = { j e. A | B =/= (/) }
27 26 a1i 
 |-  ( ph -> ( A \ { j e. A | B = (/) } ) = { j e. A | B =/= (/) } )
28 eqidd 
 |-  ( ph -> B = B )
29 15 18 10 27 28 iuneq12df 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) B = U_ j e. { j e. A | B =/= (/) } B )
30 rabid 
 |-  ( j e. { j e. A | B = (/) } <-> ( j e. A /\ B = (/) ) )
31 30 biimpi 
 |-  ( j e. { j e. A | B = (/) } -> ( j e. A /\ B = (/) ) )
32 31 adantl 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> ( j e. A /\ B = (/) ) )
33 32 simprd 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> B = (/) )
34 33 ralrimiva 
 |-  ( ph -> A. j e. { j e. A | B = (/) } B = (/) )
35 17 iunxdif3 
 |-  ( A. j e. { j e. A | B = (/) } B = (/) -> U_ j e. ( A \ { j e. A | B = (/) } ) B = U_ j e. A B )
36 34 35 syl 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) B = U_ j e. A B )
37 29 36 eqtr3d 
 |-  ( ph -> U_ j e. { j e. A | B =/= (/) } B = U_ j e. A B )
38 eqidd 
 |-  ( ph -> ( { j } X. B ) = ( { j } X. B ) )
39 15 18 10 27 38 iuneq12df 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) ( { j } X. B ) = U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) )
40 33 xpeq2d 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> ( { j } X. B ) = ( { j } X. (/) ) )
41 xp0 
 |-  ( { j } X. (/) ) = (/)
42 40 41 eqtrdi 
 |-  ( ( ph /\ j e. { j e. A | B = (/) } ) -> ( { j } X. B ) = (/) )
43 42 ralrimiva 
 |-  ( ph -> A. j e. { j e. A | B = (/) } ( { j } X. B ) = (/) )
44 17 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 ) )
45 43 44 syl 
 |-  ( ph -> U_ j e. ( A \ { j e. A | B = (/) } ) ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
46 39 45 eqtr3d 
 |-  ( ph -> U_ j e. { j e. A | B =/= (/) } ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
47 14 37 46 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 ) ) )
48 37 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 ) )
49 47 48 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 ) ) )
50 49 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 ) ) )
51 13 50 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 ) )