Metamath Proof Explorer


Theorem suppimacnv

Description: Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019) (Revised by AV, 7-Apr-2019)

Ref Expression
Assertion suppimacnv ( ( 𝑅𝑉𝑍𝑊 ) → ( 𝑅 supp 𝑍 ) = ( 𝑅 “ ( V ∖ { 𝑍 } ) ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝑡 = 𝑠 → ( 𝑥 𝑅 𝑡𝑥 𝑅 𝑠 ) )
2 1 cbvexvw ( ∃ 𝑡 𝑥 𝑅 𝑡 ↔ ∃ 𝑠 𝑥 𝑅 𝑠 )
3 breq2 ( 𝑠 = 𝑍 → ( 𝑥 𝑅 𝑠𝑥 𝑅 𝑍 ) )
4 3 anbi1d ( 𝑠 = 𝑍 → ( ( 𝑥 𝑅 𝑠 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) ↔ ( 𝑥 𝑅 𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) ) )
5 bianir ( ( 𝑡𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → 𝑥 𝑅 𝑡 )
6 vex 𝑡 ∈ V
7 breq2 ( 𝑦 = 𝑡 → ( 𝑥 𝑅 𝑦𝑥 𝑅 𝑡 ) )
8 neeq1 ( 𝑦 = 𝑡 → ( 𝑦𝑍𝑡𝑍 ) )
9 7 8 anbi12d ( 𝑦 = 𝑡 → ( ( 𝑥 𝑅 𝑦𝑦𝑍 ) ↔ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) )
10 6 9 spcev ( ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) )
11 10 ex ( 𝑥 𝑅 𝑡 → ( 𝑡𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
12 5 11 syl ( ( 𝑡𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ( 𝑡𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
13 12 ex ( 𝑡𝑍 → ( ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ( 𝑡𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) )
14 13 pm2.43a ( 𝑡𝑍 → ( ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
15 14 adantld ( 𝑡𝑍 → ( ( 𝑥 𝑅 𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
16 nne ( ¬ 𝑡𝑍𝑡 = 𝑍 )
17 notbi ( ( 𝑥 𝑅 𝑡𝑡𝑍 ) ↔ ( ¬ 𝑥 𝑅 𝑡 ↔ ¬ 𝑡𝑍 ) )
18 bianir ( ( ¬ 𝑡𝑍 ∧ ( ¬ 𝑥 𝑅 𝑡 ↔ ¬ 𝑡𝑍 ) ) → ¬ 𝑥 𝑅 𝑡 )
19 breq2 ( 𝑍 = 𝑡 → ( 𝑥 𝑅 𝑍𝑥 𝑅 𝑡 ) )
20 19 eqcoms ( 𝑡 = 𝑍 → ( 𝑥 𝑅 𝑍𝑥 𝑅 𝑡 ) )
21 pm2.24 ( 𝑥 𝑅 𝑡 → ( ¬ 𝑥 𝑅 𝑡 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
22 20 21 syl6bi ( 𝑡 = 𝑍 → ( 𝑥 𝑅 𝑍 → ( ¬ 𝑥 𝑅 𝑡 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) )
23 22 com13 ( ¬ 𝑥 𝑅 𝑡 → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) )
24 18 23 syl ( ( ¬ 𝑡𝑍 ∧ ( ¬ 𝑥 𝑅 𝑡 ↔ ¬ 𝑡𝑍 ) ) → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) )
25 24 ex ( ¬ 𝑡𝑍 → ( ( ¬ 𝑥 𝑅 𝑡 ↔ ¬ 𝑡𝑍 ) → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) ) )
26 17 25 syl5bi ( ¬ 𝑡𝑍 → ( ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) ) )
27 26 com13 ( 𝑥 𝑅 𝑍 → ( ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ( ¬ 𝑡𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) ) )
28 27 imp ( ( 𝑥 𝑅 𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ( ¬ 𝑡𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) )
29 28 com13 ( 𝑡 = 𝑍 → ( ¬ 𝑡𝑍 → ( ( 𝑥 𝑅 𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) )
30 16 29 sylbi ( ¬ 𝑡𝑍 → ( ¬ 𝑡𝑍 → ( ( 𝑥 𝑅 𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) ) )
31 30 pm2.43i ( ¬ 𝑡𝑍 → ( ( 𝑥 𝑅 𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
32 15 31 pm2.61i ( ( 𝑥 𝑅 𝑍 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) )
33 4 32 syl6bi ( 𝑠 = 𝑍 → ( ( 𝑥 𝑅 𝑠 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
34 vex 𝑠 ∈ V
35 breq2 ( 𝑦 = 𝑠 → ( 𝑥 𝑅 𝑦𝑥 𝑅 𝑠 ) )
36 neeq1 ( 𝑦 = 𝑠 → ( 𝑦𝑍𝑠𝑍 ) )
37 35 36 anbi12d ( 𝑦 = 𝑠 → ( ( 𝑥 𝑅 𝑦𝑦𝑍 ) ↔ ( 𝑥 𝑅 𝑠𝑠𝑍 ) ) )
38 34 37 spcev ( ( 𝑥 𝑅 𝑠𝑠𝑍 ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) )
39 38 ex ( 𝑥 𝑅 𝑠 → ( 𝑠𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
40 39 adantr ( ( 𝑥 𝑅 𝑠 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ( 𝑠𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
41 40 com12 ( 𝑠𝑍 → ( ( 𝑥 𝑅 𝑠 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
42 33 41 pm2.61ine ( ( 𝑥 𝑅 𝑠 ∧ ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) )
43 42 expcom ( ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ( 𝑥 𝑅 𝑠 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
44 43 exlimiv ( ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ( 𝑥 𝑅 𝑠 → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
45 44 com12 ( 𝑥 𝑅 𝑠 → ( ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
46 45 exlimiv ( ∃ 𝑠 𝑥 𝑅 𝑠 → ( ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
47 2 46 sylbi ( ∃ 𝑡 𝑥 𝑅 𝑡 → ( ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
48 47 imp ( ( ∃ 𝑡 𝑥 𝑅 𝑡 ∧ ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) )
49 48 a1i ( ( 𝑅𝑉𝑍𝑊 ) → ( ( ∃ 𝑡 𝑥 𝑅 𝑡 ∧ ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) ) )
50 49 ss2abdv ( ( 𝑅𝑉𝑍𝑊 ) → { 𝑥 ∣ ( ∃ 𝑡 𝑥 𝑅 𝑡 ∧ ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) } )
51 suppvalbr ( ( 𝑅𝑉𝑍𝑊 ) → ( 𝑅 supp 𝑍 ) = { 𝑥 ∣ ( ∃ 𝑡 𝑥 𝑅 𝑡 ∧ ∃ 𝑡 ( 𝑥 𝑅 𝑡𝑡𝑍 ) ) } )
52 cnvimadfsn ( 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) }
53 52 a1i ( ( 𝑅𝑉𝑍𝑊 ) → ( 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) } )
54 50 51 53 3sstr4d ( ( 𝑅𝑉𝑍𝑊 ) → ( 𝑅 supp 𝑍 ) ⊆ ( 𝑅 “ ( V ∖ { 𝑍 } ) ) )
55 suppimacnvss ( ( 𝑅𝑉𝑍𝑊 ) → ( 𝑅 “ ( V ∖ { 𝑍 } ) ) ⊆ ( 𝑅 supp 𝑍 ) )
56 54 55 eqssd ( ( 𝑅𝑉𝑍𝑊 ) → ( 𝑅 supp 𝑍 ) = ( 𝑅 “ ( V ∖ { 𝑍 } ) ) )