tz7.48lem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tz7.48lem		Structured version Visualization version GIF version

Theorem tz7.48lem 8242

Description: A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997.)

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

**Assertion**
Ref	Expression
tz7.48lem	⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))

Distinct variable groups: 𝑦,𝐴,𝑥 𝑥,𝐹,𝑦 𝑥,𝐴

Proof of Theorem tz7.48lem Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		r2al 3124	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
2		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)
3	2	anim1i 614	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))
4	3	imim1i 63	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
5	4	expd 415	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
6	5	2alimi 1816	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
7	1, 6	sylbi 216	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
8		r2al 3124	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
9	7, 8	sylibr 233	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
10		elequ1 2115	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
11		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
12	11	eqeq2d 2749	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑤)))
13	12	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
14	10, 13	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ((𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤))))
15	14	cbvralvw 3372	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
16	15	ralbii 3090	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
17		elequ2 2123	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
18		fveqeq2 6765	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑤)))
19	18	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (¬ (𝐹‘𝑥) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
20	17, 19	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
21	20	ralbidv 3120	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
22	21	cbvralvw 3372	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
23		elequ1 2115	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
24		fveq2 6756	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
25	24	eqeq2d 2749	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑥)))
26	25	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (¬ (𝐹‘𝑧) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
27	23, 26	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥))))
28	27	cbvralvw 3372	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
29	28	ralbii 3090	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
30		elequ2 2123	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦))
31		fveqeq2 6765	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐹‘𝑥) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)))
32	31	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ (𝐹‘𝑧) = (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
33	30, 32	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
34	33	ralbidv 3120	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
35	34	cbvralvw 3372	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
36	29, 35	bitri 274	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
37	16, 22, 36	3bitri 296	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
38		ralcom 3280	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
39	38	biimpi 215	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
40	37, 39	sylbi 216	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
41	40	ancri 549	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
42		r19.26-2 3095	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
43	41, 42	sylibr 233	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
44	9, 43	syl 17	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
45		fvres 6775	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥))
46		fvres 6775	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
47	45, 46	eqeqan12d 2752	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
48	47	ad2antrl 724	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
49		ssel 3910	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
50		ssel 3910	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On))
51	49, 50	anim12d 608	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ On ∧ 𝑦 ∈ On)))
52		pm3.48 960	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
53		oridm 901	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))
54		eqcom 2745	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥))
55	54	notbii 319	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥))
56	55	orbi1i 910	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
57	53, 56	bitr3i 276	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
58	52, 57	syl6ibr 251	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
59	58	con2d 134	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
60		eloni 6261	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ On → Ord 𝑥)
61		eloni 6261	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ On → Ord 𝑦)
62		ordtri3 6287	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 = 𝑦 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
63	62	biimprd 247	. . . . . . . . . . . . 13 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦))
64	60, 61, 63	syl2an 595	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦))
65	59, 64	syl9r 78	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
66	51, 65	syl6 35	. . . . . . . . . 10 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
67	66	imp32 418	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
68	48, 67	sylbid 239	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))
69	68	exp32 420	. . . . . . 7 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
70	69	a2d 29	. . . . . 6 ⊢ (𝐴 ⊆ On → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
71	70	2alimdv 1922	. . . . 5 ⊢ (𝐴 ⊆ On → (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
72		r2al 3124	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))
73		r2al 3124	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
74	71, 72, 73	3imtr4g 295	. . . 4 ⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
75	44, 74	syl5 34	. . 3 ⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
76	75	imdistani 568	. 2 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
77		tz7.48.1	. . . 4 ⊢ 𝐹 Fn On
78		fnssres 6539	. . . 4 ⊢ ((𝐹 Fn On ∧ 𝐴 ⊆ On) → (𝐹 ↾ 𝐴) Fn 𝐴)
79	77, 78	mpan 686	. . 3 ⊢ (𝐴 ⊆ On → (𝐹 ↾ 𝐴) Fn 𝐴)
80		dffn2 6586	. . . 4 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (𝐹 ↾ 𝐴):𝐴⟶V)
81		dff13 7109	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
82		df-f1 6423	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ^◡(𝐹 ↾ 𝐴)))
83	81, 82	bitr3i 276	. . . . 5 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ^◡(𝐹 ↾ 𝐴)))
84	83	simprbi 496	. . . 4 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
85	80, 84	sylanb 580	. . 3 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
86	79, 85	sylan 579	. 2 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
87	76, 86	syl 17	1 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∀wal 1537 = wceq 1539 ∈ wcel 2108 ∀wral 3063 Vcvv 3422 ⊆ wss 3883 ^◡ccnv 5579 ↾ cres 5582 Ord word 6250 Oncon0 6251 Fun wfun 6412 Fn wfn 6413 ⟶wf 6414 –1-1→wf1 6415 ‘cfv 6418

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-res 5592 df-ord 6254 df-on 6255 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fv 6426

This theorem is referenced by: tz7.48-2 8243 tz7.49 8246 zorn2lem4 10186

W3C validator