Theorem tz7.48lem 8428

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 3207	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
2		simpl 487	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)
3	2	anim1i 626	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))
4	3	imim1i 64	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
5	4	expd 420	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
6	5	2alimi 1839	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
7	1, 6	sylbi 220	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
8		r2al 3207	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
9	7, 8	sylibr 237	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
10		elequ1 2156	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
11		fveq2 6882	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
12	11	eqeq2d 2780	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑤)))
13	12	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
14	10, 13	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ((𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤))))
15	14	cbvralvw 3249	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
16	15	ralbii 3117	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
17		elequ2 2164	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
18		fveqeq2 6891	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑤)))
19	18	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (¬ (𝐹‘𝑥) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
20	17, 19	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
21	20	ralbidv 3194	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
22	21	cbvralvw 3249	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
23		elequ1 2156	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
24		fveq2 6882	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
25	24	eqeq2d 2780	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑥)))
26	25	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (¬ (𝐹‘𝑧) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
27	23, 26	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥))))
28	27	cbvralvw 3249	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
29	28	ralbii 3117	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
30		elequ2 2164	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦))
31		fveqeq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐹‘𝑥) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)))
32	31	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ (𝐹‘𝑧) = (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
33	30, 32	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
34	33	ralbidv 3194	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
35	34	cbvralvw 3249	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
36	29, 35	bitri 278	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
37	16, 22, 36	3bitri 300	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
38		ralcom 3299	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
39	38	biimpi 219	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
40	37, 39	sylbi 220	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
41	40	ancri 558	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
42		r19.26-2 3156	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
43	41, 42	sylibr 237	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
44	9, 43	syl 18	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
45		fvres 6901	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥))
46		fvres 6901	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
47	45, 46	eqeqan12d 2783	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
48	47	ad2antrl 740	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
49		ssel 3939	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
50		ssel 3939	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On))
51	49, 50	anim12d 620	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ On ∧ 𝑦 ∈ On)))
52		pm3.48 978	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
53		oridm 917	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))
54		eqcom 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥))
55	54	notbii 323	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥))
56	55	orbi1i 926	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
57	53, 56	bitr3i 280	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
58	52, 57	imbitrrdi 255	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
59	58	con2d 135	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
60		eloni 6371	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ On → Ord 𝑥)
61		eloni 6371	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ On → Ord 𝑦)
62		ordtri3 6398	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 = 𝑦 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
63	62	biimprd 251	. . . . . . . . . . . . 13 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦))
64	60, 61, 63	syl2an 607	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦))
65	59, 64	syl9r 79	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
66	51, 65	syl6 36	. . . . . . . . . 10 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
67	66	imp32 423	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
68	48, 67	sylbid 243	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))
69	68	exp32 425	. . . . . . 7 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
70	69	a2d 30	. . . . . 6 ⊢ (𝐴 ⊆ On → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
71	70	2alimdv 1945	. . . . 5 ⊢ (𝐴 ⊆ On → (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
72		r2al 3207	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))
73		r2al 3207	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
74	71, 72, 73	3imtr4g 299	. . . 4 ⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
75	44, 74	syl5 35	. . 3 ⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
76	75	imdistani 578	. 2 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
77		tz7.48.1	. . . 4 ⊢ 𝐹 Fn On
78		fnssres 6659	. . . 4 ⊢ ((𝐹 Fn On ∧ 𝐴 ⊆ On) → (𝐹 ↾ 𝐴) Fn 𝐴)
79	77, 78	mpan 702	. . 3 ⊢ (𝐴 ⊆ On → (𝐹 ↾ 𝐴) Fn 𝐴)
80		dffn2 6708	. . . 4 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (𝐹 ↾ 𝐴):𝐴⟶V)
81		dff13 7253	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
82		df-f1 6542	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ◡(𝐹 ↾ 𝐴)))
83	81, 82	bitr3i 280	. . . . 5 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ◡(𝐹 ↾ 𝐴)))
84	83	simprbi 502	. . . 4 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ◡(𝐹 ↾ 𝐴))
85	80, 84	sylanb 592	. . 3 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ◡(𝐹 ↾ 𝐴))
86	79, 85	sylan 591	. 2 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ◡(𝐹 ↾ 𝐴))
87	76, 86	syl 18	1 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  ∀wal 1565   = wceq 1567   ∈ wcel 2149  ∀wral 3085  Vcvv 3463   ⊆ wss 3913  ^◡ccnv 5661   ↾ cres 5664  Ord word 6360  Oncon0 6361  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  –1-1→wf1 6534  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-res 5674  df-ord 6364  df-on 6365  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fv 6545

This theorem is referenced by:  tz7.48-2  8429  tz7.49  8432  zorn2lem4  10483