Metamath Proof Explorer

Theorem aciunf1

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

Ref Expression
Hypotheses aciunf1.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
aciunf1.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
Assertion aciunf1 ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) )

Proof

Step Hyp Ref Expression
1 aciunf1.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 aciunf1.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3 ssrab2 ⊢ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ⊆ 𝐴
4 ssexg ⊢ ( ( { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ∈ V )
5 3 1 4 sylancr ⊢ ( 𝜑 → { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ∈ V )
6 rabid ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ↔ ( 𝑗 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) )
7 6 bilani ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ) → ( 𝑗 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) )
8 7 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ) → 𝐵 ≠ ∅ )
9 nfrab1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ }
10 7 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ) → 𝑗 ∈ 𝐴 )
11 10 2 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ) → 𝐵 ∈ 𝑊 )
12 5 8 9 11 aciunf1lem ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 –1-1→ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑘 ∈ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) )
13 eqidd ⊢ ( 𝜑 → 𝑓 = 𝑓 )
14 nfv ⊢ Ⅎ 𝑗 𝜑
15 nfcv ⊢ Ⅎ 𝑗 𝐴
16 nfrab1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ }
17 15 16 nfdif ⊢ Ⅎ 𝑗 ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } )
18 difrab ⊢ ( { 𝑗 ∈ 𝐴 ∣ ⊤ } ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) = { 𝑗 ∈ 𝐴 ∣ ( ⊤ ∧ ¬ 𝐵 = ∅ ) }
19 15 rabtru ⊢ { 𝑗 ∈ 𝐴 ∣ ⊤ } = 𝐴
20 19 difeq1i ⊢ ( { 𝑗 ∈ 𝐴 ∣ ⊤ } ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) = ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } )
21 truan ⊢ ( ( ⊤ ∧ ¬ 𝐵 = ∅ ) ↔ ¬ 𝐵 = ∅ )
22 df-ne ⊢ ( 𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅ )
23 21 22 bitr4i ⊢ ( ( ⊤ ∧ ¬ 𝐵 = ∅ ) ↔ 𝐵 ≠ ∅ )
24 23 rabbii ⊢ { 𝑗 ∈ 𝐴 ∣ ( ⊤ ∧ ¬ 𝐵 = ∅ ) } = { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ }
25 18 20 24 3eqtr3i ⊢ ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) = { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ }
26 25 a1i ⊢ ( 𝜑 → ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) = { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } )
27 eqidd ⊢ ( 𝜑 → 𝐵 = 𝐵 )
28 14 17 9 26 27 iuneq12df ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) 𝐵 = ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 )
29 rabid ⊢ ( 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ↔ ( 𝑗 ∈ 𝐴 ∧ 𝐵 = ∅ ) )
30 29 bilani ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → ( 𝑗 ∈ 𝐴 ∧ 𝐵 = ∅ ) )
31 30 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → 𝐵 = ∅ )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐵 = ∅ )
33 16 iunxdif3 ⊢ ( ∀ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } 𝐵 = ∅ → ∪ 𝑗 ∈ ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵 )
34 32 33 syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵 )
35 28 34 eqtr3d ⊢ ( 𝜑 → ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵 )
36 eqidd ⊢ ( 𝜑 → ( { 𝑗 } × 𝐵 ) = ( { 𝑗 } × 𝐵 ) )
37 14 17 9 26 36 iuneq12df ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ( { 𝑗 } × 𝐵 ) )
38 31 xpeq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → ( { 𝑗 } × 𝐵 ) = ( { 𝑗 } × ∅ ) )
39 xp0 ⊢ ( { 𝑗 } × ∅ ) = ∅
40 38 39 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) → ( { 𝑗 } × 𝐵 ) = ∅ )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ( { 𝑗 } × 𝐵 ) = ∅ )
42 16 iunxdif3 ⊢ ( ∀ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ( { 𝑗 } × 𝐵 ) = ∅ → ∪ 𝑗 ∈ ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
43 41 42 syl ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝐴 ∖ { 𝑗 ∈ 𝐴 ∣ 𝐵 = ∅ } ) ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
44 37 43 eqtr3d ⊢ ( 𝜑 → ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
45 13 35 44 f1eq123d ⊢ ( 𝜑 → ( 𝑓 : ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 –1-1→ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ( { 𝑗 } × 𝐵 ) ↔ 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
46 35 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ↔ ∀ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) )
47 45 46 anbi12d ⊢ ( 𝜑 → ( ( 𝑓 : ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 –1-1→ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑘 ∈ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) ↔ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) ) )
48 47 exbidv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 –1-1→ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑘 ∈ ∪ 𝑗 ∈ { 𝑗 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) ↔ ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) ) )
49 12 48 mpbid ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) )