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 8462

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 3184	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
2		simpl 481	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)
3	2	anim1i 613	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))
4	3	imim1i 63	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
5	4	expd 414	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
6	5	2alimi 1806	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
7	1, 6	sylbi 216	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
8		r2al 3184	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
9	7, 8	sylibr 233	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
10		elequ1 2105	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
11		fveq2 6896	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
12	11	eqeq2d 2736	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑤)))
13	12	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
14	10, 13	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ((𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤))))
15	14	cbvralvw 3224	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
16	15	ralbii 3082	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
17		elequ2 2113	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
18		fveqeq2 6905	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑤)))
19	18	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (¬ (𝐹‘𝑥) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
20	17, 19	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
21	20	ralbidv 3167	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
22	21	cbvralvw 3224	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
23		elequ1 2105	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
24		fveq2 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
25	24	eqeq2d 2736	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑥)))
26	25	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (¬ (𝐹‘𝑧) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
27	23, 26	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥))))
28	27	cbvralvw 3224	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
29	28	ralbii 3082	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
30		elequ2 2113	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦))
31		fveqeq2 6905	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐹‘𝑥) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)))
32	31	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ (𝐹‘𝑧) = (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
33	30, 32	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
34	33	ralbidv 3167	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
35	34	cbvralvw 3224	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
36	29, 35	bitri 274	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
37	16, 22, 36	3bitri 296	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
38		ralcom 3276	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
39	38	biimpi 215	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
40	37, 39	sylbi 216	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
41	40	ancri 548	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
42		r19.26-2 3127	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
43	41, 42	sylibr 233	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
44	9, 43	syl 17	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
45		fvres 6915	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥))
46		fvres 6915	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
47	45, 46	eqeqan12d 2739	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
48	47	ad2antrl 726	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
49		ssel 3970	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
50		ssel 3970	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On))
51	49, 50	anim12d 607	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ On ∧ 𝑦 ∈ On)))
52		pm3.48 961	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
53		oridm 902	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))
54		eqcom 2732	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥))
55	54	notbii 319	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥))
56	55	orbi1i 911	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
57	53, 56	bitr3i 276	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
58	52, 57	imbitrrdi 251	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
59	58	con2d 134	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
60		eloni 6381	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ On → Ord 𝑥)
61		eloni 6381	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ On → Ord 𝑦)
62		ordtri3 6407	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 = 𝑦 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
63	62	biimprd 247	. . . . . . . . . . . . 13 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦))
64	60, 61, 63	syl2an 594	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦))
65	59, 64	syl9r 78	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
66	51, 65	syl6 35	. . . . . . . . . 10 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
67	66	imp32 417	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
68	48, 67	sylbid 239	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))
69	68	exp32 419	. . . . . . 7 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
70	69	a2d 29	. . . . . 6 ⊢ (𝐴 ⊆ On → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
71	70	2alimdv 1913	. . . . 5 ⊢ (𝐴 ⊆ On → (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
72		r2al 3184	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))
73		r2al 3184	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
74	71, 72, 73	3imtr4g 295	. . . 4 ⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
75	44, 74	syl5 34	. . 3 ⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
76	75	imdistani 567	. 2 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
77		tz7.48.1	. . . 4 ⊢ 𝐹 Fn On
78		fnssres 6679	. . . 4 ⊢ ((𝐹 Fn On ∧ 𝐴 ⊆ On) → (𝐹 ↾ 𝐴) Fn 𝐴)
79	77, 78	mpan 688	. . 3 ⊢ (𝐴 ⊆ On → (𝐹 ↾ 𝐴) Fn 𝐴)
80		dffn2 6725	. . . 4 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (𝐹 ↾ 𝐴):𝐴⟶V)
81		dff13 7265	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
82		df-f1 6554	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ^◡(𝐹 ↾ 𝐴)))
83	81, 82	bitr3i 276	. . . . 5 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ^◡(𝐹 ↾ 𝐴)))
84	83	simprbi 495	. . . 4 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
85	80, 84	sylanb 579	. . 3 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
86	79, 85	sylan 578	. 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 394 ∨ wo 845 ∀wal 1531 = wceq 1533 ∈ wcel 2098 ∀wral 3050 Vcvv 3461 ⊆ wss 3944 ^◡ccnv 5677 ↾ cres 5680 Ord word 6370 Oncon0 6371 Fun wfun 6543 Fn wfn 6544 ⟶wf 6545 –1-1→wf1 6546 ‘cfv 6549

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-res 5690 df-ord 6374 df-on 6375 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fv 6557

This theorem is referenced by: tz7.48-2 8463 tz7.49 8466 zorn2lem4 10524

W3C validator