Theorem suppimacnv 8200

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 5146	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝑥𝑅𝑡 ↔ 𝑥𝑅𝑠))
2	1	cbvexvw 2035	. . . . . . 7 ⊢ (∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠)
3		breq2 5146	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑍 → (𝑥𝑅𝑠 ↔ 𝑥𝑅𝑍))
4	3	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))))
5		bianir 1058	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ≠ 𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → 𝑥𝑅𝑡)
6		vex 3483	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑡 ∈ V
7		breq2 5146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑡 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑡))
8		neeq1 3002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑡 → (𝑦 ≠ 𝑍 ↔ 𝑡 ≠ 𝑍))
9	7, 8	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑡 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑡 ∧ 𝑡 ≠ 𝑍)))
10	6, 9	spcev 3605	. . . . . . . . . . . . . . . . . . 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 2943	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ≠ 𝑍 ↔ 𝑡 = 𝑍)
17		notbi 319	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍))
18		bianir 1058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝑡 ≠ 𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) → ¬ 𝑥𝑅𝑡)
19		breq2 5146	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑍 = 𝑡 → (𝑥𝑅𝑍 ↔ 𝑥𝑅𝑡))
20	19	eqcoms 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = 𝑍 → (𝑥𝑅𝑍 ↔ 𝑥𝑅𝑡))
21		pm2.24 124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑅𝑡 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
22	20, 21	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑍 → (𝑥𝑅𝑍 → (¬ 𝑥𝑅𝑡 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
23	22	com13 88	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑥𝑅𝑡 → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
24	18, 23	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ 𝑡 ≠ 𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
25	24	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑡 ≠ 𝑍 → ((¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))))
26	17, 25	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))))
27	26	com13 88	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑅𝑍 → ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (¬ 𝑡 ≠ 𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))))
28	27	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (¬ 𝑡 ≠ 𝑍 → (𝑡 = 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
29	28	com13 88	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑍 → (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
30	16, 29	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ≠ 𝑍 → (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))))
31	30	pm2.43i 52	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ≠ 𝑍 → ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
32	15, 31	pm2.61i 182	. . . . . . . . . . . . 13 ⊢ ((𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
33	4, 32	biimtrdi 253	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
34		vex 3483	. . . . . . . . . . . . . . . 16 ⊢ 𝑠 ∈ V
35		breq2 5146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑠))
36		neeq1 3002	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑦 ≠ 𝑍 ↔ 𝑠 ≠ 𝑍))
37	35, 36	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑠 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍)))
38	34, 37	spcev 3605	. . . . . . . . . . . . . . 15 ⊢ ((𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
39	38	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑅𝑠 → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
40	39	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
41	40	com12 32	. . . . . . . . . . . 12 ⊢ (𝑠 ≠ 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
42	33, 41	pm2.61ine 3024	. . . . . . . . . . 11 ⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
43	42	expcom 413	. . . . . . . . . 10 ⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
44	43	exlimiv 1929	. . . . . . . . 9 ⊢ (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
45	44	com12 32	. . . . . . . 8 ⊢ (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
46	45	exlimiv 1929	. . . . . . 7 ⊢ (∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
47	2, 46	sylbi 217	. . . . . 6 ⊢ (∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
48	47	imp 406	. . . . 5 ⊢ ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
49	48	a1i 11	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
50	49	ss2abdv 4065	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)})
51		suppvalbr 8190	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))})
52		cnvimadfsn 8198	. . . 4 ⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)}
53	52	a1i 11	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)})
54	50, 51, 53	3sstr4d 4038	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) ⊆ (◡𝑅 “ (V ∖ {𝑍})))
55		suppimacnvss 8199	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
56	54, 55	eqssd 4000	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  {cab 2713   ≠ wne 2939  Vcvv 3479   ∖ cdif 3947  {csn 4625   class class class wbr 5142  ^◡ccnv 5683   “ cima 5687  (class class class)co 7432   supp csupp 8186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-supp 8187

This theorem is referenced by:  fsuppeq  8201  fsuppeqg  8202  suppun  8210  mptsuppdifd  8212  suppco  8232  fidmfisupp  9413  fdmfisuppfi  9415  fsuppun  9428  fsuppco  9443  gsumval3a  19922  gsumzf1o  19931  gsumzaddlem  19940  gsumzmhm  19956  gsumzoppg  19963  deg1val  26136  suppun2  32694  suppss3  32736  ffsrn  32741  fpwrelmapffslem  32744  sitgclg  34345  eulerpartlemmf  34378  eulerpartlemgf  34382