Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem tz7.48lem 2993

Description: A way of showing an ordinal function is one-to-one.

**Hypothesis**
Ref	Expression
tz7.48.1	⊢ F Fn On

**Assertion**
Ref	Expression
tz7.48lem	⊢ ((A ⊆ On ∧ ∀x ∈ A ∀y ∈ x ¬ (F ‘x) = (F ‘y)) → Fun ^◡(F ↾ A))

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

**Proof of Theorem tz7.48lem**
Step	Hyp	Ref	Expression
1		fvres 2840	. . . . . . . . . . . 12 ⊢ (x ∈ A → ((F ↾ A) ‘x) = (F ‘x))
2		fvres 2840	. . . . . . . . . . . 12 ⊢ (y ∈ A → ((F ↾ A) ‘y) = (F ‘y))
3	1, 2	cleqan12d 1116	. . . . . . . . . . 11 ⊢ ((x ∈ A ∧ y ∈ A) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) ↔ (F ‘x) = (F ‘y)))
4	3	ad2antrl 322	. . . . . . . . . 10 ⊢ ((A ⊆ On ∧ ((x ∈ A ∧ y ∈ A) ∧ ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))))) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) ↔ (F ‘x) = (F ‘y)))
5		ssel 1502	. . . . . . . . . . . . 13 ⊢ (A ⊆ On → (x ∈ A → x ∈ On))
6		ssel 1502	. . . . . . . . . . . . 13 ⊢ (A ⊆ On → (y ∈ A → y ∈ On))
7	5, 6	anim12d 431	. . . . . . . . . . . 12 ⊢ (A ⊆ On → ((x ∈ A ∧ y ∈ A) → (x ∈ On ∧ y ∈ On)))
8		pm3.48 430	. . . . . . . . . . . . . . 15 ⊢ (((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) → ((x ∈ y ∨ y ∈ x) → (¬ (F ‘y) = (F ‘x) ∨ ¬ (F ‘x) = (F ‘y))))
9		oridm 208	. . . . . . . . . . . . . . . 16 ⊢ ((¬ (F ‘x) = (F ‘y) ∨ ¬ (F ‘x) = (F ‘y)) ↔ ¬ (F ‘x) = (F ‘y))
10		cleqcom 1103	. . . . . . . . . . . . . . . . . 18 ⊢ ((F ‘x) = (F ‘y) ↔ (F ‘y) = (F ‘x))
11	10	negbii 162	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (F ‘x) = (F ‘y) ↔ ¬ (F ‘y) = (F ‘x))
12	11	orbi1i 215	. . . . . . . . . . . . . . . 16 ⊢ ((¬ (F ‘x) = (F ‘y) ∨ ¬ (F ‘x) = (F ‘y)) ↔ (¬ (F ‘y) = (F ‘x) ∨ ¬ (F ‘x) = (F ‘y)))
13	9, 12	bitr3 153	. . . . . . . . . . . . . . 15 ⊢ (¬ (F ‘x) = (F ‘y) ↔ (¬ (F ‘y) = (F ‘x) ∨ ¬ (F ‘x) = (F ‘y)))
14	8, 13	syl6ibr 186	. . . . . . . . . . . . . 14 ⊢ (((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) → ((x ∈ y ∨ y ∈ x) → ¬ (F ‘x) = (F ‘y)))
15	14	con2d 83	. . . . . . . . . . . . 13 ⊢ (((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) → ((F ‘x) = (F ‘y) → ¬ (x ∈ y ∨ y ∈ x)))
16		ordtri3 2234	. . . . . . . . . . . . . . 15 ⊢ ((Ord x ∧ Ord y) → (x = y ↔ ¬ (x ∈ y ∨ y ∈ x)))
17	16	biimprd 136	. . . . . . . . . . . . . 14 ⊢ ((Ord x ∧ Ord y) → (¬ (x ∈ y ∨ y ∈ x) → x = y))
18		eloni 2209	. . . . . . . . . . . . . 14 ⊢ (x ∈ On → Ord x)
19		eloni 2209	. . . . . . . . . . . . . 14 ⊢ (y ∈ On → Ord y)
20	17, 18, 19	syl2an 349	. . . . . . . . . . . . 13 ⊢ ((x ∈ On ∧ y ∈ On) → (¬ (x ∈ y ∨ y ∈ x) → x = y))
21	15, 20	syl9r 56	. . . . . . . . . . . 12 ⊢ ((x ∈ On ∧ y ∈ On) → (((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) → ((F ‘x) = (F ‘y) → x = y)))
22	7, 21	syl6 23	. . . . . . . . . . 11 ⊢ (A ⊆ On → ((x ∈ A ∧ y ∈ A) → (((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) → ((F ‘x) = (F ‘y) → x = y))))
23	22	imp32 281	. . . . . . . . . 10 ⊢ ((A ⊆ On ∧ ((x ∈ A ∧ y ∈ A) ∧ ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))))) → ((F ‘x) = (F ‘y) → x = y))
24	4, 23	sylbid 178	. . . . . . . . 9 ⊢ ((A ⊆ On ∧ ((x ∈ A ∧ y ∈ A) ∧ ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))))) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y))
25	24	exp32 294	. . . . . . . 8 ⊢ (A ⊆ On → ((x ∈ A ∧ y ∈ A) → (((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y))))
26	25	a2d 15	. . . . . . 7 ⊢ (A ⊆ On → (((x ∈ A ∧ y ∈ A) → ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y)))) → ((x ∈ A ∧ y ∈ A) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y))))
27	26	19.20dv 946	. . . . . 6 ⊢ (A ⊆ On → (∀y((x ∈ A ∧ y ∈ A) → ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y)))) → ∀y((x ∈ A ∧ y ∈ A) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y))))
28	27	19.20dv 946	. . . . 5 ⊢ (A ⊆ On → (∀x∀y((x ∈ A ∧ y ∈ A) → ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y)))) → ∀x∀y((x ∈ A ∧ y ∈ A) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y))))
29		r2al 1231	. . . . 5 ⊢ (∀x ∈ A ∀y ∈ A ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) ↔ ∀x∀y((x ∈ A ∧ y ∈ A) → ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y)))))
30		r2al 1231	. . . . 5 ⊢ (∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y) ↔ ∀x∀y((x ∈ A ∧ y ∈ A) → (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)))
31	28, 29, 30	3imtr4g 426	. . . 4 ⊢ (A ⊆ On → (∀x ∈ A ∀y ∈ A ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) → ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)))
32		pm3.26 256	. . . . . . . . . . 11 ⊢ ((x ∈ A ∧ y ∈ A) → x ∈ A)
33	32	anim1i 269	. . . . . . . . . 10 ⊢ (((x ∈ A ∧ y ∈ A) ∧ y ∈ x) → (x ∈ A ∧ y ∈ x))
34	33	syl4 19	. . . . . . . . 9 ⊢ (((x ∈ A ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y)) → (((x ∈ A ∧ y ∈ A) ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y)))
35	34	exp3a 292	. . . . . . . 8 ⊢ (((x ∈ A ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y)) → ((x ∈ A ∧ y ∈ A) → (y ∈ x → ¬ (F ‘x) = (F ‘y))))
36	35	19.20i 691	. . . . . . 7 ⊢ (∀y((x ∈ A ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y)) → ∀y((x ∈ A ∧ y ∈ A) → (y ∈ x → ¬ (F ‘x) = (F ‘y))))
37	36	19.20i 691	. . . . . 6 ⊢ (∀x∀y((x ∈ A ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y)) → ∀x∀y((x ∈ A ∧ y ∈ A) → (y ∈ x → ¬ (F ‘x) = (F ‘y))))
38		r2al 1231	. . . . . 6 ⊢ (∀x ∈ A ∀y ∈ x ¬ (F ‘x) = (F ‘y) ↔ ∀x∀y((x ∈ A ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y)))
39		r2al 1231	. . . . . 6 ⊢ (∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)) ↔ ∀x∀y((x ∈ A ∧ y ∈ A) → (y ∈ x → ¬ (F ‘x) = (F ‘y))))
40	37, 38, 39	3imtr4 192	. . . . 5 ⊢ (∀x ∈ A ∀y ∈ x ¬ (F ‘x) = (F ‘y) → ∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)))
41		eleq1 1149	. . . . . . . . . . . 12 ⊢ (y = w → (y ∈ x ↔ w ∈ x))
42		fveq2 2832	. . . . . . . . . . . . . 14 ⊢ (y = w → (F ‘y) = (F ‘w))
43	42	cleq2d 1112	. . . . . . . . . . . . 13 ⊢ (y = w → ((F ‘x) = (F ‘y) ↔ (F ‘x) = (F ‘w)))
44	43	negbid 463	. . . . . . . . . . . 12 ⊢ (y = w → (¬ (F ‘x) = (F ‘y) ↔ ¬ (F ‘x) = (F ‘w)))
45	41, 44	imbi12d 474	. . . . . . . . . . 11 ⊢ (y = w → ((y ∈ x → ¬ (F ‘x) = (F ‘y)) ↔ (w ∈ x → ¬ (F ‘x) = (F ‘w))))
46	45	cbvralv 1333	. . . . . . . . . 10 ⊢ (∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)) ↔ ∀w ∈ A (w ∈ x → ¬ (F ‘x) = (F ‘w)))
47	46	biral 1223	. . . . . . . . 9 ⊢ (∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)) ↔ ∀x ∈ A ∀w ∈ A (w ∈ x → ¬ (F ‘x) = (F ‘w)))
48		eleq2 1150	. . . . . . . . . . . 12 ⊢ (x = z → (w ∈ x ↔ w ∈ z))
49		fveq2 2832	. . . . . . . . . . . . . 14 ⊢ (x = z → (F ‘x) = (F ‘z))
50	49	cleq1d 1109	. . . . . . . . . . . . 13 ⊢ (x = z → ((F ‘x) = (F ‘w) ↔ (F ‘z) = (F ‘w)))
51	50	negbid 463	. . . . . . . . . . . 12 ⊢ (x = z → (¬ (F ‘x) = (F ‘w) ↔ ¬ (F ‘z) = (F ‘w)))
52	48, 51	imbi12d 474	. . . . . . . . . . 11 ⊢ (x = z → ((w ∈ x → ¬ (F ‘x) = (F ‘w)) ↔ (w ∈ z → ¬ (F ‘z) = (F ‘w))))
53	52	biraldv 1219	. . . . . . . . . 10 ⊢ (x = z → (∀w ∈ A (w ∈ x → ¬ (F ‘x) = (F ‘w)) ↔ ∀w ∈ A (w ∈ z → ¬ (F ‘z) = (F ‘w))))
54	53	cbvralv 1333	. . . . . . . . 9 ⊢ (∀x ∈ A ∀w ∈ A (w ∈ x → ¬ (F ‘x) = (F ‘w)) ↔ ∀z ∈ A ∀w ∈ A (w ∈ z → ¬ (F ‘z) = (F ‘w)))
55		eleq1 1149	. . . . . . . . . . . . 13 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
56		fveq2 2832	. . . . . . . . . . . . . . 15 ⊢ (w = x → (F ‘w) = (F ‘x))
57	56	cleq2d 1112	. . . . . . . . . . . . . 14 ⊢ (w = x → ((F ‘z) = (F ‘w) ↔ (F ‘z) = (F ‘x)))
58	57	negbid 463	. . . . . . . . . . . . 13 ⊢ (w = x → (¬ (F ‘z) = (F ‘w) ↔ ¬ (F ‘z) = (F ‘x)))
59	55, 58	imbi12d 474	. . . . . . . . . . . 12 ⊢ (w = x → ((w ∈ z → ¬ (F ‘z) = (F ‘w)) ↔ (x ∈ z → ¬ (F ‘z) = (F ‘x))))
60	59	cbvralv 1333	. . . . . . . . . . 11 ⊢ (∀w ∈ A (w ∈ z → ¬ (F ‘z) = (F ‘w)) ↔ ∀x ∈ A (x ∈ z → ¬ (F ‘z) = (F ‘x)))
61	60	biral 1223	. . . . . . . . . 10 ⊢ (∀z ∈ A ∀w ∈ A (w ∈ z → ¬ (F ‘z) = (F ‘w)) ↔ ∀z ∈ A ∀x ∈ A (x ∈ z → ¬ (F ‘z) = (F ‘x)))
62		eleq2 1150	. . . . . . . . . . . . 13 ⊢ (z = y → (x ∈ z ↔ x ∈ y))
63		fveq2 2832	. . . . . . . . . . . . . . 15 ⊢ (z = y → (F ‘z) = (F ‘y))
64	63	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (z = y → ((F ‘z) = (F ‘x) ↔ (F ‘y) = (F ‘x)))
65	64	negbid 463	. . . . . . . . . . . . 13 ⊢ (z = y → (¬ (F ‘z) = (F ‘x) ↔ ¬ (F ‘y) = (F ‘x)))
66	62, 65	imbi12d 474	. . . . . . . . . . . 12 ⊢ (z = y → ((x ∈ z → ¬ (F ‘z) = (F ‘x)) ↔ (x ∈ y → ¬ (F ‘y) = (F ‘x))))
67	66	biraldv 1219	. . . . . . . . . . 11 ⊢ (z = y → (∀x ∈ A (x ∈ z → ¬ (F ‘z) = (F ‘x)) ↔ ∀x ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x))))
68	67	cbvralv 1333	. . . . . . . . . 10 ⊢ (∀z ∈ A ∀x ∈ A (x ∈ z → ¬ (F ‘z) = (F ‘x)) ↔ ∀y ∈ A ∀x ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)))
69	61, 68	bitr 151	. . . . . . . . 9 ⊢ (∀z ∈ A ∀w ∈ A (w ∈ z → ¬ (F ‘z) = (F ‘w)) ↔ ∀y ∈ A ∀x ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)))
70	47, 54, 69	3bitr 155	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)) ↔ ∀y ∈ A ∀x ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)))
71		ralcom2 1314	. . . . . . . 8 ⊢ (∀y ∈ A ∀x ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)) → ∀x ∈ A ∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)))
72	70, 71	sylbi 174	. . . . . . 7 ⊢ (∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)) → ∀x ∈ A ∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)))
73	72	ancri 245	. . . . . 6 ⊢ (∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)) → (∀x ∈ A ∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ ∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y))))
74		r19.26 1289	. . . . . . . 8 ⊢ (∀y ∈ A ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) ↔ (∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y))))
75	74	biral 1223	. . . . . . 7 ⊢ (∀x ∈ A ∀y ∈ A ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) ↔ ∀x ∈ A (∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y))))
76		r19.26 1289	. . . . . . 7 ⊢ (∀x ∈ A (∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y))) ↔ (∀x ∈ A ∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ ∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y))))
77	75, 76	bitr 151	. . . . . 6 ⊢ (∀x ∈ A ∀y ∈ A ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))) ↔ (∀x ∈ A ∀y ∈ A (x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ ∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y))))
78	73, 77	sylibr 175	. . . . 5 ⊢ (∀x ∈ A ∀y ∈ A (y ∈ x → ¬ (F ‘x) = (F ‘y)) → ∀x ∈ A ∀y ∈ A ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))))
79	40, 78	syl 12	. . . 4 ⊢ (∀x ∈ A ∀y ∈ x ¬ (F ‘x) = (F ‘y) → ∀x ∈ A ∀y ∈ A ((x ∈ y → ¬ (F ‘y) = (F ‘x)) ∧ (y ∈ x → ¬ (F ‘x) = (F ‘y))))
80	31, 79	syl5 22	. . 3 ⊢ (A ⊆ On → (∀x ∈ A ∀y ∈ x ¬ (F ‘x) = (F ‘y) → ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)))
81	80	imdistani 340	. 2 ⊢ ((A ⊆ On ∧ ∀x ∈ A ∀y ∈ x ¬ (F ‘x) = (F ‘y)) → (A ⊆ On ∧ ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)))
82		f1fv 2916	. . . . . 6 ⊢ ((F ↾ A):A–1-1→V ↔ ((F ↾ A):A–→V ∧ ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)))
83		df-f1 2435	. . . . . 6 ⊢ ((F ↾ A):A–1-1→V ↔ ((F ↾ A):A–→V ∧ Fun ^◡(F ↾ A)))
84	82, 83	bitr3 153	. . . . 5 ⊢ (((F ↾ A):A–→V ∧ ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)) ↔ ((F ↾ A):A–→V ∧ Fun ^◡(F ↾ A)))
85	84	pm3.27bd 263	. . . 4 ⊢ (((F ↾ A):A–→V ∧ ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)) → Fun ^◡(F ↾ A))
86		fnf 2753	. . . 4 ⊢ ((F ↾ A) Fn A ↔ (F ↾ A):A–→V)
87	85, 86	sylanb 344	. . 3 ⊢ (((F ↾ A) Fn A ∧ ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)) → Fun ^◡(F ↾ A))
88		tz7.48.1	. . . 4 ⊢ F Fn On
89		fnssres 2734	. . . 4 ⊢ ((F Fn On ∧ A ⊆ On) → (F ↾ A) Fn A)
90	88, 89	mpan 518	. . 3 ⊢ (A ⊆ On → (F ↾ A) Fn A)
91	87, 90	sylan 343	. 2 ⊢ ((A ⊆ On ∧ ∀x ∈ A ∀y ∈ A (((F ↾ A) ‘x) = ((F ↾ A) ‘y) → x = y)) → Fun ^◡(F ↾ A))
92	81, 91	syl 12	1 ⊢ ((A ⊆ On ∧ ∀x ∈ A ∀y ∈ x ¬ (F ‘x) = (F ‘y)) → Fun ^◡(F ↾ A))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 ∀wal 672 = weq 797 ∈ wel 803 = wceq 1091 ∈ wcel 1092 ∀wral 1201 Vcvv 1348 ⊆ wss 1487 Ord word 2198 Oncon0 2199 ^◡ccnv 2409 ↾ cres 2412 Fun wfun 2416 Fn wfn 2417 –→wf 2418 –1-1→wf1 2419 ‘cfv 2422

This theorem is referenced by: tz7.48-2 2995 tz7.49 2997 abianfp 3000 zornlem4 3606

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-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 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-fv 2438

metamath.org