Theorem suppimacnv 8107

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 5096	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝑥𝑅𝑡 ↔ 𝑥𝑅𝑠))
2	1	cbvexvw 2037	. . . . . . 7 ⊢ (∃𝑡 𝑥𝑅𝑡 ↔ ∃𝑠 𝑥𝑅𝑠)
3		breq2 5096	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑍 → (𝑥𝑅𝑠 ↔ 𝑥𝑅𝑍))
4	3	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) ↔ (𝑥𝑅𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))))
5		bianir 1058	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 ≠ 𝑍 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → 𝑥𝑅𝑡)
6		vex 3440	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑡 ∈ V
7		breq2 5096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑡 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑡))
8		neeq1 2987	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑡 → (𝑦 ≠ 𝑍 ↔ 𝑡 ≠ 𝑍))
9	7, 8	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑡 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑡 ∧ 𝑡 ≠ 𝑍)))
10	6, 9	spcev 3561	. . . . . . . . . . . . . . . . . . 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 2929	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ≠ 𝑍 ↔ 𝑡 = 𝑍)
17		notbi 319	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) ↔ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍))
18		bianir 1058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((¬ 𝑡 ≠ 𝑍 ∧ (¬ 𝑥𝑅𝑡 ↔ ¬ 𝑡 ≠ 𝑍)) → ¬ 𝑥𝑅𝑡)
19		breq2 5096	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑍 = 𝑡 → (𝑥𝑅𝑍 ↔ 𝑥𝑅𝑡))
20	19	eqcoms 2737	. . . . . . . . . . . . . . . . . . . . . . . 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 3440	. . . . . . . . . . . . . . . 16 ⊢ 𝑠 ∈ V
35		breq2 5096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑠))
36		neeq1 2987	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑠 → (𝑦 ≠ 𝑍 ↔ 𝑠 ≠ 𝑍))
37	35, 36	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑠 → ((𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍) ↔ (𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍)))
38	34, 37	spcev 3561	. . . . . . . . . . . . . . 15 ⊢ ((𝑥𝑅𝑠 ∧ 𝑠 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
39	38	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝑥𝑅𝑠 → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
40	39	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → (𝑠 ≠ 𝑍 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
41	40	com12 32	. . . . . . . . . . . 12 ⊢ (𝑠 ≠ 𝑍 → ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
42	33, 41	pm2.61ine 3008	. . . . . . . . . . 11 ⊢ ((𝑥𝑅𝑠 ∧ (𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
43	42	expcom 413	. . . . . . . . . 10 ⊢ ((𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
44	43	exlimiv 1930	. . . . . . . . 9 ⊢ (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → (𝑥𝑅𝑠 → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
45	44	com12 32	. . . . . . . 8 ⊢ (𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
46	45	exlimiv 1930	. . . . . . 7 ⊢ (∃𝑠 𝑥𝑅𝑠 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
47	2, 46	sylbi 217	. . . . . 6 ⊢ (∃𝑡 𝑥𝑅𝑡 → (∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
48	47	imp 406	. . . . 5 ⊢ ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍))
49	48	a1i 11	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍)) → ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)))
50	49	ss2abdv 4018	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))} ⊆ {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)})
51		suppvalbr 8097	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑡 𝑥𝑅𝑡 ∧ ∃𝑡(𝑥𝑅𝑡 ↔ 𝑡 ≠ 𝑍))})
52		cnvimadfsn 8105	. . . 4 ⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)}
53	52	a1i 11	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)})
54	50, 51, 53	3sstr4d 3991	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) ⊆ (◡𝑅 “ (V ∖ {𝑍})))
55		suppimacnvss 8106	. 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍))
56	54, 55	eqssd 3953	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍})))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707   ≠ wne 2925  Vcvv 3436   ∖ cdif 3900  {csn 4577   class class class wbr 5092  ^◡ccnv 5618   “ cima 5622  (class class class)co 7349   supp csupp 8093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-supp 8094

This theorem is referenced by:  fsuppeq  8108  fsuppeqg  8109  suppun  8117  mptsuppdifd  8119  suppco  8139  fidmfisupp  9262  fdmfisuppfi  9264  fsuppun  9277  fsuppco  9292  gsumval3a  19782  gsumzf1o  19791  gsumzaddlem  19800  gsumzmhm  19816  gsumzoppg  19823  deg1val  25999  suppun2  32627  suppss3  32668  ffsrn  32673  fpwrelmapffslem  32676  sitgclg  34316  eulerpartlemmf  34349  eulerpartlemgf  34353