Metamath Proof Explorer

Theorem funpartlem

Description: Lemma for funpartfun . Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion funpartlem ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃ 𝑥 ( 𝐹 “ { 𝐴 } ) = { 𝑥 } )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) → 𝐴 ∈ V )
2 vsnid ⊢ 𝑥 ∈ { 𝑥 }
3 eleq2 ⊢ ( ( 𝐹 “ { 𝐴 } ) = { 𝑥 } → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ 𝑥 ∈ { 𝑥 } ) )
4 2 3 mpbiri ⊢ ( ( 𝐹 “ { 𝐴 } ) = { 𝑥 } → 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) )
5 n0i ⊢ ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) → ¬ ( 𝐹 “ { 𝐴 } ) = ∅ )
6 snprc ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
7 6 biimpi ⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
8 7 imaeq2d ⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 “ { 𝐴 } ) = ( 𝐹 “ ∅ ) )
9 ima0 ⊢ ( 𝐹 “ ∅ ) = ∅
10 8 9 eqtrdi ⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 “ { 𝐴 } ) = ∅ )
11 5 10 nsyl2 ⊢ ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) → 𝐴 ∈ V )
12 4 11 syl ⊢ ( ( 𝐹 “ { 𝐴 } ) = { 𝑥 } → 𝐴 ∈ V )
13 12 exlimiv ⊢ ( ∃ 𝑥 ( 𝐹 “ { 𝐴 } ) = { 𝑥 } → 𝐴 ∈ V )
14 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) )
15 sneq ⊢ ( 𝑦 = 𝐴 → { 𝑦 } = { 𝐴 } )
16 15 imaeq2d ⊢ ( 𝑦 = 𝐴 → ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝐴 } ) )
17 16 eqeq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 “ { 𝑦 } ) = { 𝑥 } ↔ ( 𝐹 “ { 𝐴 } ) = { 𝑥 } ) )
18 17 exbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝐹 “ { 𝑦 } ) = { 𝑥 } ↔ ∃ 𝑥 ( 𝐹 “ { 𝐴 } ) = { 𝑥 } ) )
19 vex ⊢ 𝑦 ∈ V
20 19 eldm ⊢ ( 𝑦 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃ 𝑧 𝑦 ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) 𝑧 )
21 brxp ⊢ ( 𝑦 ( V × Singletons ) 𝑧 ↔ ( 𝑦 ∈ V ∧ 𝑧 ∈ Singletons ) )
22 19 21 mpbiran ⊢ ( 𝑦 ( V × Singletons ) 𝑧 ↔ 𝑧 ∈ Singletons )
23 elsingles ⊢ ( 𝑧 ∈ Singletons ↔ ∃ 𝑥 𝑧 = { 𝑥 } )
24 22 23 bitri ⊢ ( 𝑦 ( V × Singletons ) 𝑧 ↔ ∃ 𝑥 𝑧 = { 𝑥 } )
25 24 anbi2i ⊢ ( ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑦 ( V × Singletons ) 𝑧 ) ↔ ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ ∃ 𝑥 𝑧 = { 𝑥 } ) )
26 brin ⊢ ( 𝑦 ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) 𝑧 ↔ ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑦 ( V × Singletons ) 𝑧 ) )
27 19.42v ⊢ ( ∃ 𝑥 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) ↔ ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ ∃ 𝑥 𝑧 = { 𝑥 } ) )
28 25 26 27 3bitr4i ⊢ ( 𝑦 ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) 𝑧 ↔ ∃ 𝑥 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) )
29 28 exbii ⊢ ( ∃ 𝑧 𝑦 ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) 𝑧 ↔ ∃ 𝑧 ∃ 𝑥 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) )
30 excom ⊢ ( ∃ 𝑧 ∃ 𝑥 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) ↔ ∃ 𝑥 ∃ 𝑧 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) )
31 29 30 bitri ⊢ ( ∃ 𝑧 𝑦 ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) 𝑧 ↔ ∃ 𝑥 ∃ 𝑧 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) )
32 exancom ⊢ ( ∃ 𝑧 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) ↔ ∃ 𝑧 ( 𝑧 = { 𝑥 } ∧ 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ) )
33 snex ⊢ { 𝑥 } ∈ V
34 breq2 ⊢ ( 𝑧 = { 𝑥 } → ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ↔ 𝑦 ( Image 𝐹 ∘ Singleton ) { 𝑥 } ) )
35 33 34 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑥 } ∧ 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ) ↔ 𝑦 ( Image 𝐹 ∘ Singleton ) { 𝑥 } )
36 19 33 brco ⊢ ( 𝑦 ( Image 𝐹 ∘ Singleton ) { 𝑥 } ↔ ∃ 𝑧 ( 𝑦 Singleton 𝑧 ∧ 𝑧 Image 𝐹 { 𝑥 } ) )
37 vex ⊢ 𝑧 ∈ V
38 19 37 brsingle ⊢ ( 𝑦 Singleton 𝑧 ↔ 𝑧 = { 𝑦 } )
39 38 anbi1i ⊢ ( ( 𝑦 Singleton 𝑧 ∧ 𝑧 Image 𝐹 { 𝑥 } ) ↔ ( 𝑧 = { 𝑦 } ∧ 𝑧 Image 𝐹 { 𝑥 } ) )
40 39 exbii ⊢ ( ∃ 𝑧 ( 𝑦 Singleton 𝑧 ∧ 𝑧 Image 𝐹 { 𝑥 } ) ↔ ∃ 𝑧 ( 𝑧 = { 𝑦 } ∧ 𝑧 Image 𝐹 { 𝑥 } ) )
41 snex ⊢ { 𝑦 } ∈ V
42 breq1 ⊢ ( 𝑧 = { 𝑦 } → ( 𝑧 Image 𝐹 { 𝑥 } ↔ { 𝑦 } Image 𝐹 { 𝑥 } ) )
43 41 42 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑦 } ∧ 𝑧 Image 𝐹 { 𝑥 } ) ↔ { 𝑦 } Image 𝐹 { 𝑥 } )
44 41 33 brimage ⊢ ( { 𝑦 } Image 𝐹 { 𝑥 } ↔ { 𝑥 } = ( 𝐹 “ { 𝑦 } ) )
45 eqcom ⊢ ( { 𝑥 } = ( 𝐹 “ { 𝑦 } ) ↔ ( 𝐹 “ { 𝑦 } ) = { 𝑥 } )
46 43 44 45 3bitri ⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑦 } ∧ 𝑧 Image 𝐹 { 𝑥 } ) ↔ ( 𝐹 “ { 𝑦 } ) = { 𝑥 } )
47 36 40 46 3bitri ⊢ ( 𝑦 ( Image 𝐹 ∘ Singleton ) { 𝑥 } ↔ ( 𝐹 “ { 𝑦 } ) = { 𝑥 } )
48 32 35 47 3bitri ⊢ ( ∃ 𝑧 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) ↔ ( 𝐹 “ { 𝑦 } ) = { 𝑥 } )
49 48 exbii ⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑦 ( Image 𝐹 ∘ Singleton ) 𝑧 ∧ 𝑧 = { 𝑥 } ) ↔ ∃ 𝑥 ( 𝐹 “ { 𝑦 } ) = { 𝑥 } )
50 20 31 49 3bitri ⊢ ( 𝑦 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃ 𝑥 ( 𝐹 “ { 𝑦 } ) = { 𝑥 } )
51 14 18 50 vtoclbg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃ 𝑥 ( 𝐹 “ { 𝐴 } ) = { 𝑥 } ) )
52 1 13 51 pm5.21nii ⊢ ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃ 𝑥 ( 𝐹 “ { 𝐴 } ) = { 𝑥 } )