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 biimtrdi ⊢ ( 𝑡 = 𝑍 → ( 𝑥 𝑅 𝑍 → ( ¬ 𝑥 𝑅 𝑡 → ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) ) )
23 22 com13 ⊢ ( ¬ 𝑥 𝑅 𝑡 → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) ) )
24 18 23 syl ⊢ ( ( ¬ 𝑡 ≠ 𝑍 ∧ ( ¬ 𝑥 𝑅 𝑡 ↔ ¬ 𝑡 ≠ 𝑍 ) ) → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) ) )
25 24 ex ⊢ ( ¬ 𝑡 ≠ 𝑍 → ( ( ¬ 𝑥 𝑅 𝑡 ↔ ¬ 𝑡 ≠ 𝑍 ) → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) ) ) )
26 17 25 biimtrid ⊢ ( ¬ 𝑡 ≠ 𝑍 → ( ( 𝑥 𝑅 𝑡 ↔ 𝑡 ≠ 𝑍 ) → ( 𝑥 𝑅 𝑍 → ( 𝑡 = 𝑍 → ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) ) ) )
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 biimtrdi ⊢ ( 𝑠 = 𝑍 → ( ( 𝑥 𝑅 𝑠 ∧ ( 𝑥 𝑅 𝑡 ↔ 𝑡 ≠ 𝑍 ) ) → ∃ 𝑦 ( 𝑥 𝑅 𝑦 ∧ 𝑦 ≠ 𝑍 ) ) )
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 ∖ { 𝑍 } ) ) )