Metamath Proof Explorer

Theorem mptsnunlem

Description: This is the core of the proof of mptsnun , but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020)

Ref Expression
Hypotheses mptsnun.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
mptsnun.r ⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
Assertion mptsnunlem ( 𝐵 ⊆ 𝐴 → 𝐵 = ∪ ( 𝐹 “ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mptsnun.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } )
2 mptsnun.r ⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } }
3 df-ima ⊢ ( 𝐹 “ 𝐵 ) = ran ( 𝐹 ↾ 𝐵 )
4 1 reseq1i ⊢ ( 𝐹 ↾ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) ↾ 𝐵 )
5 resmpt ⊢ ( 𝐵 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑥 } ) )
6 4 5 syl5eq ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐹 ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑥 } ) )
7 6 rneqd ⊢ ( 𝐵 ⊆ 𝐴 → ran ( 𝐹 ↾ 𝐵 ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑥 } ) )
8 rnmptsn ⊢ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑥 } ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } }
9 7 8 eqtrdi ⊢ ( 𝐵 ⊆ 𝐴 → ran ( 𝐹 ↾ 𝐵 ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
10 3 9 syl5eq ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐹 “ 𝐵 ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
11 10 unieqd ⊢ ( 𝐵 ⊆ 𝐴 → ∪ ( 𝐹 “ 𝐵 ) = ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
12 11 eleq2d ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑥 ∈ ∪ ( 𝐹 “ 𝐵 ) ↔ 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
13 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
14 eluniab ⊢ ( 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ↔ ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) )
15 ancom ⊢ ( ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) ↔ ( ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) )
16 r19.41v ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ↔ ( ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) )
17 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ) )
18 15 16 17 3bitr2i ⊢ ( ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ) )
19 eleq2 ⊢ ( 𝑢 = { 𝑥 } → ( 𝑧 ∈ 𝑢 ↔ 𝑧 ∈ { 𝑥 } ) )
20 19 anbi2d ⊢ ( 𝑢 = { 𝑥 } → ( ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ↔ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) )
21 20 adantr ⊢ ( ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) → ( ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ↔ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) )
22 21 ibi ⊢ ( ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) → ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) )
23 22 anim2i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ) → ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) )
24 23 eximi ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ 𝑢 ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) )
25 18 24 sylbi ⊢ ( ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) )
26 an12 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) ↔ ( 𝑢 = { 𝑥 } ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) )
27 26 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) ↔ ∃ 𝑥 ( 𝑢 = { 𝑥 } ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) )
28 exsimpr ⊢ ( ∃ 𝑥 ( 𝑢 = { 𝑥 } ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) )
29 27 28 sylbi ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑢 = { 𝑥 } ∧ 𝑧 ∈ { 𝑥 } ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) )
30 25 29 syl ⊢ ( ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) )
31 30 exlimiv ⊢ ( ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) )
32 14 31 sylbi ⊢ ( 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) )
33 velsn ⊢ ( 𝑧 ∈ { 𝑥 } ↔ 𝑧 = 𝑥 )
34 33 anbi2i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥 ) )
35 34 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ { 𝑥 } ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥 ) )
36 32 35 sylib ⊢ ( 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥 ) )
37 13 biimparc ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥 ) → 𝑧 ∈ 𝐵 )
38 37 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 = 𝑥 ) → 𝑧 ∈ 𝐵 )
39 36 38 syl ⊢ ( 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } → 𝑧 ∈ 𝐵 )
40 13 39 vtoclga ⊢ ( 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } → 𝑥 ∈ 𝐵 )
41 equid ⊢ 𝑥 = 𝑥
42 eqid ⊢ { 𝑥 } = { 𝑥 }
43 snex ⊢ { 𝑥 } ∈ V
44 sbcg ⊢ ( { 𝑥 } ∈ V → ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
45 43 44 ax-mp ⊢ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 )
46 eqsbc1 ⊢ ( { 𝑥 } ∈ V → ( [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ↔ { 𝑥 } = { 𝑥 } ) )
47 43 46 ax-mp ⊢ ( [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ↔ { 𝑥 } = { 𝑥 } )
48 19 adantl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ 𝑢 ↔ 𝑧 ∈ { 𝑥 } ) )
49 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) )
50 14 biimpri ⊢ ( ∃ 𝑢 ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
51 50 19.23bi ⊢ ( ( 𝑧 ∈ 𝑢 ∧ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } ) → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
52 51 expcom ⊢ ( ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } → ( 𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
53 49 52 sylbir ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
54 53 19.23bi ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ 𝑢 → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
55 48 54 sylbird ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
56 55 sbcth ⊢ ( { 𝑥 } ∈ V → [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) ) )
57 43 56 ax-mp ⊢ [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
58 sbcimg ⊢ ( { 𝑥 } ∈ V → ( [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) ) ↔ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) ) ) )
59 43 58 ax-mp ⊢ ( [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) ) ↔ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) ) )
60 57 59 mpbi ⊢ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
61 sbcan ⊢ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐵 ∧ 𝑢 = { 𝑥 } ) ↔ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐵 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) )
62 nfv ⊢ Ⅎ 𝑢 𝑧 ∈ { 𝑥 }
63 nfab1 ⊢ Ⅎ 𝑢 { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } }
64 63 nfuni ⊢ Ⅎ 𝑢 ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } }
65 64 nfcri ⊢ Ⅎ 𝑢 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } }
66 62 65 nfim ⊢ Ⅎ 𝑢 ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
67 43 66 sbcgfi ⊢ ( [ { 𝑥 } / 𝑢 ] ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) ↔ ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
68 60 61 67 3imtr3i ⊢ ( ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐵 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
69 45 47 68 syl2anbr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ { 𝑥 } = { 𝑥 } ) → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
70 42 69 mpan2 ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑧 ∈ { 𝑥 } → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
71 33 70 syl5bir ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑧 = 𝑥 → 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
72 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ↔ 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
73 71 72 mpbidi ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑧 = 𝑥 → 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
74 73 com12 ⊢ ( 𝑧 = 𝑥 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
75 74 sbimi ⊢ ( [ 𝑥 / 𝑧 ] 𝑧 = 𝑥 → [ 𝑥 / 𝑧 ] ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
76 equsb3 ⊢ ( [ 𝑥 / 𝑧 ] 𝑧 = 𝑥 ↔ 𝑥 = 𝑥 )
77 sbv ⊢ ( [ 𝑥 / 𝑧 ] ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
78 75 76 77 3imtr3i ⊢ ( 𝑥 = 𝑥 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ) )
79 41 78 ax-mp ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } )
80 40 79 impbii ⊢ ( 𝑥 ∈ ∪ { 𝑢 ∣ ∃ 𝑥 ∈ 𝐵 𝑢 = { 𝑥 } } ↔ 𝑥 ∈ 𝐵 )
81 12 80 bitrdi ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝑥 ∈ ∪ ( 𝐹 “ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
82 81 eqrdv ⊢ ( 𝐵 ⊆ 𝐴 → ∪ ( 𝐹 “ 𝐵 ) = 𝐵 )
83 82 eqcomd ⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 = ∪ ( 𝐹 “ 𝐵 ) )