Theorem suppimacnv 7961

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

Assertion

Ref	Expression
suppimacnv	⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍})))

Proof of Theorem suppimacnv

Dummy variables 𝑥 𝑦 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5074	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝑥𝑅𝑡 ↔ 𝑥𝑅𝑠))
2	1	cbvexvw 2041	. . . . . . 7 ⊢ (∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠)
3		breq2 5074	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑍 → (𝑥𝑅𝑠 ↔ 𝑥𝑅𝑍))
4	3	anbi1d 629	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))))
5		bianir 1055	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ≠ 𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → 𝑥𝑅𝑡)
6		vex 3426	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑡 ∈ V
7		breq2 5074	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑡 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑡))
8		neeq1 3005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑡 → (𝑦 ≠ 𝑍 ↔ 𝑡 ≠ 𝑍))
9	7, 8	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑡 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑡 ∧ 𝑡 ≠ 𝑍)))
10	6, 9	spcev 3535	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥𝑅𝑡 ∧ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
11	10	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑅𝑡 → (𝑡 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
12	5, 11	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ≠ 𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (𝑡 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
13	12	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ≠ 𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑡 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
14	13	pm2.43a 54	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ≠ 𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
15	14	adantld 490	. . . . . . . . . . . . . 14 ⊢ (𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
16		nne 2946	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ≠ 𝑍 ↔ 𝑡 = 𝑍)
17		notbi 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍))
18		bianir 1055	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝑡 ≠ 𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) → ¬ 𝑥𝑅𝑡)
19		breq2 5074	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑍 = 𝑡 → (𝑥𝑅𝑍 ↔ 𝑥𝑅𝑡))
20	19	eqcoms 2746	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑍 → (𝑥𝑅𝑍 ↔ 𝑥𝑅𝑡))
21		pm2.24 124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑅𝑡 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
22	20, 21	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑍 → (𝑥𝑅𝑍 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
23	22	com13 88	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑥𝑅𝑡 → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
24	18, 23	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑡 ≠ 𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
25	24	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑡 ≠ 𝑍 → ((¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))))
26	17, 25	syl5bi 241	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))))
27	26	com13 88	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑅𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (¬ 𝑡 ≠ 𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))))
28	27	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (¬ 𝑡 ≠ 𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
29	28	com13 88	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
30	16, 29	sylbi 216	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ≠ 𝑍 → (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
31	30	pm2.43i 52	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
32	15, 31	pm2.61i 182	. . . . . . . . . . . . 13 ⊢ ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
33	4, 32	syl6bi 252	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
34		vex 3426	. . . . . . . . . . . . . . . 16 ⊢ 𝑠 ∈ V
35		breq2 5074	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑠))
36		neeq1 3005	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑦 ≠ 𝑍 ↔ 𝑠 ≠ 𝑍))
37	35, 36	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑠 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍)))
38	34, 37	spcev 3535	. . . . . . . . . . . . . . 15 ⊢ ((𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
39	38	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑅𝑠 → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
40	39	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
41	40	com12 32	. . . . . . . . . . . 12 ⊢ (𝑠 ≠ 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
42	33, 41	pm2.61ine 3027	. . . . . . . . . . 11 ⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
43	42	expcom 413	. . . . . . . . . 10 ⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
44	43	exlimiv 1934	. . . . . . . . 9 ⊢ (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
45	44	com12 32	. . . . . . . 8 ⊢ (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
46	45	exlimiv 1934	. . . . . . 7 ⊢ (∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
47	2, 46	sylbi 216	. . . . . 6 ⊢ (∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
48	47	imp 406	. . . . 5 ⊢ ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
49	48	a1i 11	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
50	49	ss2abdv 3993	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)})
51		suppvalbr 7952	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))})
52		cnvimadfsn 7959	. . . 4 ⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)}
53	52	a1i 11	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)})
54	50, 51, 53	3sstr4d 3964	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) ⊆ (◡𝑅 “ (V ∖ {𝑍})))
55		suppimacnvss 7960	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
56	54, 55	eqssd 3934	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715   ≠ wne 2942  Vcvv 3422   ∖ cdif 3880  {csn 4558   class class class wbr 5070  ^◡ccnv 5579   “ cima 5583  (class class class)co 7255   supp csupp 7948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-supp 7949

This theorem is referenced by:  frnsuppeq  7962  frnsuppeqg  7963  suppun  7971  mptsuppdifd  7973  suppco  7993  fdmfisuppfi  9067  fsuppun  9077  fsuppco  9091  gsumval3a  19419  gsumzf1o  19428  gsumzaddlem  19437  gsumzmhm  19453  gsumzoppg  19460  deg1val  25166  suppss3  30961  ffsrn  30966  fpwrelmapffslem  30969  sitgclg  32209  eulerpartlemmf  32242  eulerpartlemgf  32246  fidmfisupp  42628