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 8481

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 3195	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
2		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴)
3	2	anim1i 615	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))
4	3	imim1i 63	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
5	4	expd 415	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
6	5	2alimi 1812	. . . . . . 7 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
7	1, 6	sylbi 217	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
8		r2al 3195	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
9	7, 8	sylibr 234	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
10		elequ1 2115	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
11		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤))
12	11	eqeq2d 2748	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑤 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑤)))
13	12	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑤 → (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
14	10, 13	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ((𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤))))
15	14	cbvralvw 3237	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
16	15	ralbii 3093	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))
17		elequ2 2123	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
18		fveqeq2 6915	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑤)))
19	18	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (¬ (𝐹‘𝑥) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
20	17, 19	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
21	20	ralbidv 3178	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))))
22	21	cbvralvw 3237	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))
23		elequ1 2115	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
24		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
25	24	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑥)))
26	25	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (¬ (𝐹‘𝑧) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
27	23, 26	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥))))
28	27	cbvralvw 3237	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
29	28	ralbii 3093	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))
30		elequ2 2123	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦))
31		fveqeq2 6915	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐹‘𝑥) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)))
32	31	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ (𝐹‘𝑧) = (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
33	30, 32	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
34	33	ralbidv 3178	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))))
35	34	cbvralvw 3237	. . . . . . . . . 10 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
36	29, 35	bitri 275	. . . . . . . . 9 ⊢ (∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
37	16, 22, 36	3bitri 297	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
38		ralcom 3289	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
39	38	biimpi 216	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
40	37, 39	sylbi 217	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))
41	40	ancri 549	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
42		r19.26-2 3138	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
43	41, 42	sylibr 234	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
44	9, 43	syl 17	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
45		fvres 6925	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥))
46		fvres 6925	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
47	45, 46	eqeqan12d 2751	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
48	47	ad2antrl 728	. . . . . . . . 9 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
49		ssel 3977	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
50		ssel 3977	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On))
51	49, 50	anim12d 609	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ On ∧ 𝑦 ∈ On)))
52		pm3.48 966	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))
53		oridm 905	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))
54		eqcom 2744	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥))
55	54	notbii 320	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥))
56	55	orbi1i 914	. . . . . . . . . . . . . . 15 ⊢ ((¬ (𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
57	53, 56	bitr3i 277	. . . . . . . . . . . . . 14 ⊢ (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
58	52, 57	imbitrrdi 252	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))
59	58	con2d 134	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
60		eloni 6394	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ On → Ord 𝑥)
61		eloni 6394	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ On → Ord 𝑦)
62		ordtri3 6420	. . . . . . . . . . . . . 14 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 = 𝑦 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥)))
63	62	biimprd 248	. . . . . . . . . . . . 13 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦))
64	60, 61, 63	syl2an 596	. . . . . . . . . . . 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 240	. . . . . . . 8 ⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))
69	68	exp32 420	. . . . . . 7 ⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
70	69	a2d 29	. . . . . 6 ⊢ (𝐴 ⊆ On → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
71	70	2alimdv 1918	. . . . 5 ⊢ (𝐴 ⊆ On → (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))))
72		r2al 3195	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))))
73		r2al 3195	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
74	71, 72, 73	3imtr4g 296	. . . 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 6691	. . . 4 ⊢ ((𝐹 Fn On ∧ 𝐴 ⊆ On) → (𝐹 ↾ 𝐴) Fn 𝐴)
79	77, 78	mpan 690	. . 3 ⊢ (𝐴 ⊆ On → (𝐹 ↾ 𝐴) Fn 𝐴)
80		dffn2 6738	. . . 4 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (𝐹 ↾ 𝐴):𝐴⟶V)
81		dff13 7275	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))
82		df-f1 6566	. . . . . 6 ⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ^◡(𝐹 ↾ 𝐴)))
83	81, 82	bitr3i 277	. . . . 5 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ^◡(𝐹 ↾ 𝐴)))
84	83	simprbi 496	. . . 4 ⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
85	80, 84	sylanb 581	. . 3 ⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
86	79, 85	sylan 580	. 2 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))
87	76, 86	syl 17	1 ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ^◡(𝐹 ↾ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∀wal 1538 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ⊆ wss 3951 ^◡ccnv 5684 ↾ cres 5687 Ord word 6383 Oncon0 6384 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 ‘cfv 6561

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-res 5697 df-ord 6387 df-on 6388 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fv 6569

This theorem is referenced by: tz7.48-2 8482 tz7.49 8485 zorn2lem4 10539

W3C validator