Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem f1oweOLD 2944

Description: Well-ordering of isomorphic relations.

**Hypothesis**
Ref	Expression
f1oweOLD.1	⊢ R = {⟨x, y⟩∣(F ‘x)S(F ‘y)}

**Assertion**
Ref	Expression
f1oweOLD	⊢ (F:A–1-1-onto→B → (S We B → R We A))

Distinct variable group(s): x,y,S x,F,y

**Proof of Theorem f1oweOLD**
Step	Hyp	Ref	Expression
1		df-f1o 2437	. . . . 5 ⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))
2	1	pm3.27bd 263	. . . 4 ⊢ (F:A–1-1-onto→B → F:A–onto→B)
3		df-fo 2436	. . . . 5 ⊢ (F:A–onto→B ↔ (F Fn A ∧ ran F = B))
4		freq2 2175	. . . . . . 7 ⊢ (ran F = B → (S Fr ran F ↔ S Fr B))
5	4	biimprd 136	. . . . . 6 ⊢ (ran F = B → (S Fr B → S Fr ran F))
6		df-fn 2433	. . . . . . 7 ⊢ (F Fn A ↔ (Fun F ∧ dom F = A))
7		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ z ∈ V
8	7	funimaex 2716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun F → (F “ z) ∈ V)
9		sseq1 1521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (w = (F “ z) → (w ⊆ ran F ↔ (F “ z) ⊆ ran F))
10		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w = (F “ z) → (w = ∅ ↔ (F “ z) = ∅))
11	10	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (w = (F “ z) → (¬ w = ∅ ↔ ¬ (F “ z) = ∅))
12	9, 11	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (w = (F “ z) → ((w ⊆ ran F ∧ ¬ w = ∅) ↔ ((F “ z) ⊆ ran F ∧ ¬ (F “ z) = ∅)))
13		raleq 1324	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (w = (F “ z) → (∀f ∈ w ¬ fSu ↔ ∀f ∈ (F “ z) ¬ fSu))
14	13	rexeqd 1328	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (w = (F “ z) → (∃u ∈ w ∀f ∈ w ¬ fSu ↔ ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu))
15	12, 14	imbi12d 474	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (w = (F “ z) → (((w ⊆ ran F ∧ ¬ w = ∅) → ∃u ∈ w ∀f ∈ w ¬ fSu) ↔ (((F “ z) ⊆ ran F ∧ ¬ (F “ z) = ∅) → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu)))
16	15	cla4gv 1396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((F “ z) ∈ V → (∀w((w ⊆ ran F ∧ ¬ w = ∅) → ∃u ∈ w ∀f ∈ w ¬ fSu) → (((F “ z) ⊆ ran F ∧ ¬ (F “ z) = ∅) → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu)))
17		funfvima2 2905	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun F ∧ z ⊆ dom F) → (w ∈ z → (F ‘w) ∈ (F “ z)))
18		n0i 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((F ‘w) ∈ (F “ z) → ¬ (F “ z) = ∅)
19	17, 18	syl6 23	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun F ∧ z ⊆ dom F) → (w ∈ z → ¬ (F “ z) = ∅))
20	19	19.23adv 954	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((Fun F ∧ z ⊆ dom F) → (∃w w ∈ z → ¬ (F “ z) = ∅))
21		n0 1714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ z = ∅ ↔ ∃w w ∈ z)
22	20, 21	syl5ib 181	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Fun F ∧ z ⊆ dom F) → (¬ z = ∅ → ¬ (F “ z) = ∅))
23	22	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((Fun F ∧ z ⊆ dom F) ∧ ¬ z = ∅) → ¬ (F “ z) = ∅)
24		imassrn 2611	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (F “ z) ⊆ ran F
25	23, 24	jctil 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Fun F ∧ z ⊆ dom F) ∧ ¬ z = ∅) → ((F “ z) ⊆ ran F ∧ ¬ (F “ z) = ∅))
26	16, 25	syl7 24	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((F “ z) ∈ V → (∀w((w ⊆ ran F ∧ ¬ w = ∅) → ∃u ∈ w ∀f ∈ w ¬ fSu) → (((Fun F ∧ z ⊆ dom F) ∧ ¬ z = ∅) → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu)))
27	8, 26	syl 12	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun F → (∀w((w ⊆ ran F ∧ ¬ w = ∅) → ∃u ∈ w ∀f ∈ w ¬ fSu) → (((Fun F ∧ z ⊆ dom F) ∧ ¬ z = ∅) → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu)))
28		df-fr 2169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (S Fr ran F ↔ ∀w((w ⊆ ran F ∧ ¬ w = ∅) → ∃u ∈ w ∀f ∈ w ¬ fSu))
29	27, 28	syl5ib 181	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun F → (S Fr ran F → (((Fun F ∧ z ⊆ dom F) ∧ ¬ z = ∅) → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu)))
30	29	com23 32	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun F → (((Fun F ∧ z ⊆ dom F) ∧ ¬ z = ∅) → (S Fr ran F → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu)))
31	30	exp3a 292	. . . . . . . . . . . . . . . . 17 ⊢ (Fun F → ((Fun F ∧ z ⊆ dom F) → (¬ z = ∅ → (S Fr ran F → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu))))
32	31	anabsi5 377	. . . . . . . . . . . . . . . 16 ⊢ ((Fun F ∧ z ⊆ dom F) → (¬ z = ∅ → (S Fr ran F → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu)))
33	32	imp3a 279	. . . . . . . . . . . . . . 15 ⊢ ((Fun F ∧ z ⊆ dom F) → ((¬ z = ∅ ∧ S Fr ran F) → ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu))
34		fores 2794	. . . . . . . . . . . . . . . 16 ⊢ ((Fun F ∧ z ⊆ dom F) → (F ↾ z):z–onto→(F “ z))
35		breq1 2065	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((F ↾ z) ‘v) = f → (((F ↾ z) ‘v)S((F ↾ z) ‘w) ↔ fS((F ↾ z) ‘w)))
36	35	negbid 463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((F ↾ z) ‘v) = f → (¬ ((F ↾ z) ‘v)S((F ↾ z) ‘w) ↔ ¬ fS((F ↾ z) ‘w)))
37	36	cbvfo 2923	. . . . . . . . . . . . . . . . . . 19 ⊢ ((F ↾ z):z–onto→(F “ z) → (∀v ∈ z ¬ ((F ↾ z) ‘v)S((F ↾ z) ‘w) ↔ ∀f ∈ (F “ z) ¬ fS((F ↾ z) ‘w)))
38	37	birexdv 1220	. . . . . . . . . . . . . . . . . 18 ⊢ ((F ↾ z):z–onto→(F “ z) → (∃w ∈ z ∀v ∈ z ¬ ((F ↾ z) ‘v)S((F ↾ z) ‘w) ↔ ∃w ∈ z ∀f ∈ (F “ z) ¬ fS((F ↾ z) ‘w)))
39		breq2 2066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((F ↾ z) ‘w) = u → (fS((F ↾ z) ‘w) ↔ fSu))
40	39	negbid 463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((F ↾ z) ‘w) = u → (¬ fS((F ↾ z) ‘w) ↔ ¬ fSu))
41	40	biraldv 1219	.v. . . . . . . . . . . . . . . . . 19 ⊢ (((F ↾ z) ‘w) = u → (∀f ∈ (F “ z) ¬ fS((F ↾ z) ‘w) ↔ ∀f ∈ (F “ z) ¬ fSu))
42	41	cbvexfo 2924	. . . . . . . . . . . . . . . . . 18 ⊢ ((F ↾ z):z–onto→(F “ z) → (∃w ∈ z ∀f ∈ (F “ z) ¬ fS((F ↾ z) ‘w) ↔ ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu))
43	38, 42	bitrd 406	. . . . . . . . . . . . . . . . 17 ⊢ ((F ↾ z):z–onto→(F “ z) → (∃w ∈ z ∀v ∈ z ¬ ((F ↾ z) ‘v)S((F ↾ z) ‘w) ↔ ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu))
44		fvres 2840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (v ∈ z → ((F ↾ z) ‘v) = (F ‘v))
45		fvres 2840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w ∈ z → ((F ↾ z) ‘w) = (F ‘w))
46	44, 45	breqan12rd 2075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w ∈ z ∧ v ∈ z) → (((F ↾ z) ‘v)S((F ↾ z) ‘w) ↔ (F ‘v)S(F ‘w)))
47		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ v ∈ V
48		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ w ∈ V
49		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (x = v → (F ‘x) = (F ‘v))
50	49	breq1d 2071	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = v → ((F ‘x)S(F ‘y) ↔ (F ‘v)S(F ‘y)))
51		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (y = w → (F ‘y) = (F ‘w))
52	51	breq2d 2072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = w → ((F ‘v)S(F ‘y) ↔ (F ‘v)S(F ‘w)))
53		f1oweOLD.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ R = {⟨x, y⟩∣(F ‘x)S(F ‘y)}
54	47, 48, 50, 52, 53	brab 2118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (vRw ↔ (F ‘v)S(F ‘w))
55	46, 54	syl6rbbr 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((w ∈ z ∧ v ∈ z) → (vRw ↔ ((F ↾ z) ‘v)S((F ↾ z) ‘w)))
56	55	negbid 463	. . . . . . . . . . . . . . . . . . 19 ⊢ ((w ∈ z ∧ v ∈ z) → (¬ vRw ↔ ¬ ((F ↾ z) ‘v)S((F ↾ z) ‘w)))
57	56	biraldva 1215	. . . . . . . . . . . . . . . . . 18 ⊢ (w ∈ z → (∀v ∈ z ¬ vRw ↔ ∀v ∈ z ¬ ((F ↾ z) ‘v)S((F ↾ z) ‘w)))
58	57	birexa 1229	. . . . . . . . . . . . . . . . 17 ⊢ (∃w ∈ z ∀v ∈ z ¬ vRw ↔ ∃w ∈ z ∀v ∈ z ¬ ((F ↾ z) ‘v)S((F ↾ z) ‘w))
59	43, 58	syl5bb 410	. . . . . . . . . . . . . . . 16 ⊢ ((F ↾ z):z–onto→(F “ z) → (∃w ∈ z ∀v ∈ z ¬ vRw ↔ ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu))
60	34, 59	syl 12	. . . . . . . . . . . . . . 15 ⊢ ((Fun F ∧ z ⊆ dom F) → (∃w ∈ z ∀v ∈ z ¬ vRw ↔ ∃u ∈ (F “ z)∀f ∈ (F “ z) ¬ fSu))
61	33, 60	sylibrd 179	. . . . . . . . . . . . . 14 ⊢ ((Fun F ∧ z ⊆ dom F) → ((¬ z = ∅ ∧ S Fr ran F) → ∃w ∈ z ∀v ∈ z ¬ vRw))
62	61	exp4b 296	. . . . . . . . . . . . 13 ⊢ (Fun F → (z ⊆ dom F → (¬ z = ∅ → (S Fr ran F → ∃w ∈ z ∀v ∈ z ¬ vRw))))
63	62	com34 36	. . . . . . . . . . . 12 ⊢ (Fun F → (z ⊆ dom F → (S Fr ran F → (¬ z = ∅ → ∃w ∈ z ∀v ∈ z ¬ vRw))))
64	63	com23 32	. . . . . . . . . . 11 ⊢ (Fun F → (S Fr ran F → (z ⊆ dom F → (¬ z = ∅ → ∃w ∈ z ∀v ∈ z ¬ vRw))))
65	64	imp4a 282	. . . . . . . . . 10 ⊢ (Fun F → (S Fr ran F → ((z ⊆ dom F ∧ ¬ z = ∅) → ∃w ∈ z ∀v ∈ z ¬ vRw)))
66	65	19.21adv 945	. . . . . . . . 9 ⊢ (Fun F → (S Fr ran F → ∀z((z ⊆ dom F ∧ ¬ z = ∅) → ∃w ∈ z ∀v ∈ z ¬ vRw)))
67		df-fr 2169	. . . . . . . . 9 ⊢ (R Fr dom F ↔ ∀z((z ⊆ dom F ∧ ¬ z = ∅) → ∃w ∈ z ∀v ∈ z ¬ vRw))
68	66, 67	syl6ibr 186	. . . . . . . 8 ⊢ (Fun F → (S Fr ran F → R Fr dom F))
69		freq2 2175	. . . . . . . . 9 ⊢ (dom F = A → (R Fr dom F ↔ R Fr A))
70	69	biimpd 135	. . . . . . . 8 ⊢ (dom F = A → (R Fr dom F → R Fr A))
71	68, 70	sylan9 359	. . . . . . 7 ⊢ ((Fun F ∧ dom F = A) → (S Fr ran F → R Fr A))
72	6, 71	sylbi 174	. . . . . 6 ⊢ (F Fn A → (S Fr ran F → R Fr A))
73	5, 72	sylan9r 360	. . . . 5 ⊢ ((F Fn A ∧ ran F = B) → (S Fr B → R Fr A))
74	3, 73	sylbi 174	. . . 4 ⊢ (F:A–onto→B → (S Fr B → R Fr A))
75	2, 74	syl 12	. . 3 ⊢ (F:A–1-1-onto→B → (S Fr B → R Fr A))
76		fveq2 2832	. . . . . . . . . . 11 ⊢ (x = w → (F ‘x) = (F ‘w))
77	76	breq1d 2071	. . . . . . . . . 10 ⊢ (x = w → ((F ‘x)S(F ‘y) ↔ (F ‘w)S(F ‘y)))
78		fveq2 2832	. . . . . . . . . . 11 ⊢ (y = v → (F ‘y) = (F ‘v))
79	78	breq2d 2072	. . . . . . . . . 10 ⊢ (y = v → ((F ‘w)S(F ‘y) ↔ (F ‘w)S(F ‘v)))
80	48, 47, 77, 79, 53	brab 2118	. . . . . . . . 9 ⊢ (wRv ↔ (F ‘w)S(F ‘v))
81	80	a1i 7	. . . . . . . 8 ⊢ ((F:A–1-1→B ∧ (w ∈ A ∧ v ∈ A)) → (wRv ↔ (F ‘w)S(F ‘v)))
82		f1fveq 2918	. . . . . . . . 9 ⊢ ((F:A–1-1→B ∧ (w ∈ A ∧ v ∈ A)) → ((F ‘w) = (F ‘v) ↔ w = v))
83	82	bicomd 399	. . . . . . . 8 ⊢ ((F:A–1-1→B ∧ (w ∈ A ∧ v ∈ A)) → (w = v ↔ (F ‘w) = (F ‘v)))
84	54	a1i 7	. . . . . . . 8 ⊢ ((F:A–1-1→B ∧ (w ∈ A ∧ v ∈ A)) → (vRw ↔ (F ‘v)S(F ‘w)))
85	81, 83, 84	bi3ord 635	. . . . . . 7 ⊢ ((F:A–1-1→B ∧ (w ∈ A ∧ v ∈ A)) → ((wRv ∨ w = v ∨ vRw) ↔ ((F ‘w)S(F ‘v) ∨ (F ‘w) = (F ‘v) ∨ (F ‘v)S(F ‘w))))
86	85	bi2raldva 1233	. . . . . 6 ⊢ (F:A–1-1→B → (∀w ∈ A ∀v ∈ A (wRv ∨ w = v ∨ vRw) ↔ ∀w ∈ A ∀v ∈ A ((F ‘w)S(F ‘v) ∨ (F ‘w) = (F ‘v) ∨ (F ‘v)S(F ‘w))))
87		breq1 2065	. . . . . . . . . 10 ⊢ ((F ‘w) = u → ((F ‘w)S(F ‘v) ↔ uS(F ‘v)))
88		cleq1 1107	. . . . . . . . . 10 ⊢ ((F ‘w) = u → ((F ‘w) = (F ‘v) ↔ u = (F ‘v)))
89		breq2 2066	. . . . . . . . . 10 ⊢ ((F ‘w) = u → ((F ‘v)S(F ‘w) ↔ (F ‘v)Su))
90	87, 88, 89	bi3ord 635	. . . . . . . . 9 ⊢ ((F ‘w) = u → (((F ‘w)S(F ‘v) ∨ (F ‘w) = (F ‘v) ∨ (F ‘v)S(F ‘w)) ↔ (uS(F ‘v) ∨ u = (F ‘v) ∨ (F ‘v)Su)))
91	90	biraldv 1219	. . . . . . . 8 ⊢ ((F ‘w) = u → (∀v ∈ A ((F ‘w)S(F ‘v) ∨ (F ‘w) = (F ‘v) ∨ (F ‘v)S(F ‘w)) ↔ ∀v ∈ A (uS(F ‘v) ∨ u = (F ‘v) ∨ (F ‘v)Su)))
92	91	cbvfo 2923	. . . . . . 7 ⊢ (F:A–onto→B → (∀w ∈ A ∀v ∈ A ((F ‘w)S(F ‘v) ∨ (F ‘w) = (F ‘v) ∨ (F ‘v)S(F ‘w)) ↔ ∀u ∈ B ∀v ∈ A (uS(F ‘v) ∨ u = (F ‘v) ∨ (F ‘v)Su)))
93		breq2 2066	. . . . . . . . . 10 ⊢ ((F ‘v) = f → (uS(F ‘v) ↔ uSf))
94		cleq2 1110	. . . . . . . . . 10 ⊢ ((F ‘v) = f → (u = (F ‘v) ↔ u = f))
95		breq1 2065	. . . . . . . . . 10 ⊢ ((F ‘v) = f → ((F ‘v)Su ↔ fSu))
96	93, 94, 95	bi3ord 635	. . . . . . . . 9 ⊢ ((F ‘v) = f → ((uS(F ‘v) ∨ u = (F ‘v) ∨ (F ‘v)Su) ↔ (uSf ∨ u = f ∨ fSu)))
97	96	cbvfo 2923	. . . . . . . 8 ⊢ (F:A–onto→B → (∀v ∈ A (uS(F ‘v) ∨ u = (F ‘v) ∨ (F ‘v)Su) ↔ ∀f ∈ B (uSf ∨ u = f ∨ fSu)))
98	97	biraldv 1219	. . . . . . 7 ⊢ (F:A–onto→B → (∀u ∈ B ∀v ∈ A (uS(F ‘v) ∨ u = (F ‘v) ∨ (F ‘v)Su) ↔ ∀u ∈ B ∀f ∈ B (uSf ∨ u = f ∨ fSu)))
99	92, 98	bitrd 406	. . . . . 6 ⊢ (F:A–onto→B → (∀w ∈ A ∀v ∈ A ((F ‘w)S(F ‘v) ∨ (F ‘w) = (F ‘v) ∨ (F ‘v)S(F ‘w)) ↔ ∀u ∈ B ∀f ∈ B (uSf ∨ u = f ∨ fSu)))
100	86, 99	sylan9bb 418	. . . . 5 ⊢ ((F:A–1-1→B ∧ F:A–onto→B) → (∀w ∈ A ∀v ∈ A (wRv ∨ w = v ∨ vRw) ↔ ∀u ∈ B ∀f ∈ B (uSf ∨ u = f ∨ fSu)))
101	1, 100	sylbi 174	. . . 4 ⊢ (F:A–1-1-onto→B → (∀w ∈ A ∀v ∈ A (wRv ∨ w = v ∨ vRw) ↔ ∀u ∈ B ∀f ∈ B (uSf ∨ u = f ∨ fSu)))
102	101	biimprd 136	. . 3 ⊢ (F:A–1-1-onto→B → (∀u ∈ B ∀f ∈ B (uSf ∨ u = f ∨ fSu) → ∀w ∈ A ∀v ∈ A (wRv ∨ w = v ∨ vRw)))
103	75, 102	anim12d 431	. 2 ⊢ (F:A–1-1-onto→B → ((S Fr B ∧ ∀u ∈ B ∀f ∈ B (uSf ∨ u = f ∨ fSu)) → (R Fr A ∧ ∀w ∈ A ∀v ∈ A (wRv ∨ w = v ∨ vRw))))
104		dfwe2 2187	. 2 ⊢ (S We B ↔ (S Fr B ∧ ∀u ∈ B ∀f ∈ B (uSf ∨ u = f ∨ fSu)))
105		dfwe2 2187	. 2 ⊢ (R We A ↔ (R Fr A ∧ ∀w ∈ A ∀v ∈ A (wRv ∨ w = v ∨ vRw)))
106	103, 104, 105	3imtr4g 426	1 ⊢ (F:A–1-1-onto→B → (S We B → R We A))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∨ w3o 580 ∀wal 672 ∃wex 678 = weq 797 ∈ wel 803 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 Vcvv 1348 ⊆ wss 1487 ∅c0 1707 class class class wbr 2054 {copab 2055 Fr wfr 2061 We wwe 2062 dom cdm 2410 ran crn 2411 ↾ cres 2412 “ cima 2413 Fun wfun 2416 Fn wfn 2417 –1-1→wf1 2419 –onto→wfo 2420 –1-1-onto→wf1o 2421 ‘cfv 2422

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-3or 582 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-ral 1205 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-tp 1814 df-op 1815 df-uni 1920 df-br 2063 df-opab 2098 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 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

metamath.org