Theorem infmap2lem1 4951

Description: Lemma for infmap2 4953. Technical result that is used several times.

Hypotheses

Ref	Expression
infmap2lem.1	⊢ A ∈ V
infmap2lem.2	⊢ B ∈ V
infmap2lem.3	⊢ R = {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)}

Assertion

Ref	Expression
infmap2lem1	⊢ ((f ⊆ R ∧ f Fn dom R) → (v ∈ {x∣(x ⊆ A ∧ x ≈ B)} → (v ⊆ A ∧ (f ‘v):B–onto→v)))

Distinct variable group(s):   x,z,w,v,f,A   x,B,z,w,f,v   v,R,f

Proof of Theorem infmap2lem1

Step	Hyp	Ref	Expression
1		ssel 1502	. . . . . 6 ⊢ (f ⊆ R → (⟨v, (f ‘v)⟩ ∈ f → ⟨v, (f ‘v)⟩ ∈ R))
2		infmap2lem.3	. . . . . . . . 9 ⊢ R = {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)}
3	2	eleq2i 1153	. . . . . . . 8 ⊢ (⟨v, (f ‘v)⟩ ∈ R ↔ ⟨v, (f ‘v)⟩ ∈ {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)})
4		visset 1350	. . . . . . . . 9 ⊢ v ∈ V
5		fvex 2838	. . . . . . . . 9 ⊢ (f ‘v) ∈ V
6		sseq1 1521	. . . . . . . . . . 11 ⊢ (z = v → (z ⊆ A ↔ v ⊆ A))
7		breq1 2065	. . . . . . . . . . 11 ⊢ (z = v → (z ≈ B ↔ v ≈ B))
8	6, 7	anbi12d 476	. . . . . . . . . 10 ⊢ (z = v → ((z ⊆ A ∧ z ≈ B) ↔ (v ⊆ A ∧ v ≈ B)))
9		foeq3 2786	. . . . . . . . . 10 ⊢ (z = v → (w:B–onto→z ↔ w:B–onto→v))
10	8, 9	anbi12d 476	. . . . . . . . 9 ⊢ (z = v → (((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z) ↔ ((v ⊆ A ∧ v ≈ B) ∧ w:B–onto→v)))
11		foeq1 2784	. . . . . . . . . 10 ⊢ (w = (f ‘v) → (w:B–onto→v ↔ (f ‘v):B–onto→v))
12	11	anbi2d 468	. . . . . . . . 9 ⊢ (w = (f ‘v) → (((v ⊆ A ∧ v ≈ B) ∧ w:B–onto→v) ↔ ((v ⊆ A ∧ v ≈ B) ∧ (f ‘v):B–onto→v)))
13	4, 5, 10, 12	opelopab 2117	. . . . . . . 8 ⊢ (⟨v, (f ‘v)⟩ ∈ {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)} ↔ ((v ⊆ A ∧ v ≈ B) ∧ (f ‘v):B–onto→v))
14	3, 13	bitr 151	. . . . . . 7 ⊢ (⟨v, (f ‘v)⟩ ∈ R ↔ ((v ⊆ A ∧ v ≈ B) ∧ (f ‘v):B–onto→v))
15		pm3.26 256	. . . . . . . 8 ⊢ ((v ⊆ A ∧ v ≈ B) → v ⊆ A)
16	15	anim1i 269	. . . . . . 7 ⊢ (((v ⊆ A ∧ v ≈ B) ∧ (f ‘v):B–onto→v) → (v ⊆ A ∧ (f ‘v):B–onto→v))
17	14, 16	sylbi 174	. . . . . 6 ⊢ (⟨v, (f ‘v)⟩ ∈ R → (v ⊆ A ∧ (f ‘v):B–onto→v))
18	1, 17	syl6 23	. . . . 5 ⊢ (f ⊆ R → (⟨v, (f ‘v)⟩ ∈ f → (v ⊆ A ∧ (f ‘v):B–onto→v)))
19		fnopfv 2887	. . . . 5 ⊢ ((f Fn dom R ∧ v ∈ dom R) → ⟨v, (f ‘v)⟩ ∈ f)
20	18, 19	syl5 22	. . . 4 ⊢ (f ⊆ R → ((f Fn dom R ∧ v ∈ dom R) → (v ⊆ A ∧ (f ‘v):B–onto→v)))
21	20	exp3a 292	. . 3 ⊢ (f ⊆ R → (f Fn dom R → (v ∈ dom R → (v ⊆ A ∧ (f ‘v):B–onto→v))))
22	21	imp 277	. 2 ⊢ ((f ⊆ R ∧ f Fn dom R) → (v ∈ dom R → (v ⊆ A ∧ (f ‘v):B–onto→v)))
23	2	dmeqi 2532	. . . . 5 ⊢ dom R = dom {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)}
24		dmopab 2539	. . . . 5 ⊢ dom {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)} = {z∣∃w((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)}
25		anass 336	. . . . . . 7 ⊢ (((z ⊆ A ∧ z ≈ B) ∧ ∃w w:B–onto→z) ↔ (z ⊆ A ∧ (z ≈ B ∧ ∃w w:B–onto→z)))
26		19.42v 966	. . . . . . 7 ⊢ (∃w((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z) ↔ ((z ⊆ A ∧ z ≈ B) ∧ ∃w w:B–onto→z))
27		infmap2lem.2	. . . . . . . . . . 11 ⊢ B ∈ V
28	27	ensym 3317	. . . . . . . . . 10 ⊢ (z ≈ B → B ≈ z)
29		visset 1350	. . . . . . . . . . . 12 ⊢ z ∈ V
30	29	bren 3282	. . . . . . . . . . 11 ⊢ (B ≈ z ↔ ∃w w:B–1-1-onto→z)
31		f1ofo 2806	. . . . . . . . . . . 12 ⊢ (w:B–1-1-onto→z → w:B–onto→z)
32	31	19.22i 723	. . . . . . . . . . 11 ⊢ (∃w w:B–1-1-onto→z → ∃w w:B–onto→z)
33	30, 32	sylbi 174	. . . . . . . . . 10 ⊢ (B ≈ z → ∃w w:B–onto→z)
34	28, 33	syl 12	. . . . . . . . 9 ⊢ (z ≈ B → ∃w w:B–onto→z)
35	34	pm4.71i 483	. . . . . . . 8 ⊢ (z ≈ B ↔ (z ≈ B ∧ ∃w w:B–onto→z))
36	35	anbi2i 367	. . . . . . 7 ⊢ ((z ⊆ A ∧ z ≈ B) ↔ (z ⊆ A ∧ (z ≈ B ∧ ∃w w:B–onto→z)))
37	25, 26, 36	3bitr4 158	. . . . . 6 ⊢ (∃w((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z) ↔ (z ⊆ A ∧ z ≈ B))
38	37	biabi 1181	. . . . 5 ⊢ {z∣∃w((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)} = {z∣(z ⊆ A ∧ z ≈ B)}
39	23, 24, 38	3eqtr 1123	. . . 4 ⊢ dom R = {z∣(z ⊆ A ∧ z ≈ B)}
40		sseq1 1521	. . . . . 6 ⊢ (z = x → (z ⊆ A ↔ x ⊆ A))
41		breq1 2065	. . . . . 6 ⊢ (z = x → (z ≈ B ↔ x ≈ B))
42	40, 41	anbi12d 476	. . . . 5 ⊢ (z = x → ((z ⊆ A ∧ z ≈ B) ↔ (x ⊆ A ∧ x ≈ B)))
43	42	cbvabv 1424	. . . 4 ⊢ {z∣(z ⊆ A ∧ z ≈ B)} = {x∣(x ⊆ A ∧ x ≈ B)}
44	39, 43	eqtr 1119	. . 3 ⊢ dom R = {x∣(x ⊆ A ∧ x ≈ B)}
45	44	eleq2i 1153	. 2 ⊢ (v ∈ dom R ↔ v ∈ {x∣(x ⊆ A ∧ x ≈ B)})
46	22, 45	syl5ibr 182	1 ⊢ ((f ⊆ R ∧ f Fn dom R) → (v ∈ {x∣(x ⊆ A ∧ x ≈ B)} → (v ⊆ A ∧ (f ‘v):B–onto→v)))

Syntax hints:   → wi 2   ∧ wa 196  ∃wex 678   = weq 797  {cab 1090   = wceq 1091   ∈ wcel 1092  Vcvv 1348   ⊆ wss 1487  ⟨cop 1810   class class class wbr 2054  {copab 2055  dom cdm 2410   Fn wfn 2417  –onto→wfo 2420  –1-1-onto→wf1o 2421   ‘cfv 2422   ≈ cen 3271

This theorem is referenced by:  infmap2lem2 4952

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-er 3200  df-en 3274

metamath.org