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