Metamath Proof Explorer

Theorem tz7.48lem

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

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

Proof

Step Hyp Ref Expression
1 tz7.48.1 ⊢ 𝐹 Fn On
2 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
3 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
4 3 anim1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
5 4 imim1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
6 5 expd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
7 6 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
8 2 7 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
9 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
10 8 9 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
11 elequ1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) )
12 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
13 12 eqeq2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) )
14 13 notbid ⊢ ( 𝑦 = 𝑤 → ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) )
15 11 14 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
16 15 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) )
17 16 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) )
18 elequ2 ⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) )
19 fveqeq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
20 19 notbid ⊢ ( 𝑥 = 𝑧 → ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
21 18 20 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑤 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑤 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
22 21 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ) )
23 22 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
24 elequ1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
25 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
26 25 eqeq2d ⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
27 26 notbid ⊢ ( 𝑤 = 𝑥 → ( ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
28 24 27 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑥 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
29 28 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
30 29 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) )
31 elequ2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦 ) )
32 fveqeq2 ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
33 32 notbid ⊢ ( 𝑧 = 𝑦 → ( ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
34 31 33 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
35 34 ralbidv ⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
36 35 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
37 30 36 bitri ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑤 ∈ 𝑧 → ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
38 17 23 37 3bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
39 ralcom2w ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
40 38 39 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
41 40 ancri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
42 r19.26-2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
43 41 42 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
44 10 43 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
45 fvres ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
46 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
47 45 46 eqeqan12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
48 47 ad2antrl ⊢ ( ( 𝐴 ⊆ On ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
49 ssel ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On ) )
50 ssel ⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On ) )
51 49 50 anim12d ⊢ ( 𝐴 ⊆ On → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) )
52 pm3.48 ⊢ ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ( ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
53 oridm ⊢ ( ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
54 eqcom ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
55 54 notbii ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
56 55 orbi1i ⊢ ( ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
57 53 56 bitr3i ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
58 52 57 syl6ibr ⊢ ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
59 58 con2d ⊢ ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) )
60 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
61 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
62 ordtri3 ⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( 𝑥 = 𝑦 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) )
63 62 biimprd ⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → 𝑥 = 𝑦 ) )
64 60 61 63 syl2an ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → 𝑥 = 𝑦 ) )
65 59 64 syl9r ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
66 51 65 syl6 ⊢ ( 𝐴 ⊆ On → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
67 66 imp32 ⊢ ( ( 𝐴 ⊆ On ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
68 48 67 sylbid ⊢ ( ( 𝐴 ⊆ On ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
69 68 exp32 ⊢ ( 𝐴 ⊆ On → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
70 69 a2d ⊢ ( 𝐴 ⊆ On → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
71 70 2alimdv ⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
72 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
73 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
74 71 72 73 3imtr4g ⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
75 44 74 syl5 ⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
76 75 imdistani ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
77 fnssres ⊢ ( ( 𝐹 Fn On ∧ 𝐴 ⊆ On ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
78 1 77 mpan ⊢ ( 𝐴 ⊆ On → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
79 dffn2 ⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V )
80 dff13 ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ V ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
81 df-f1 ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ V ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ Fun ◡ ( 𝐹 ↾ 𝐴 ) ) )
82 80 81 bitr3i ⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ Fun ◡ ( 𝐹 ↾ 𝐴 ) ) )
83 82 simprbi ⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )
84 79 83 sylanb ⊢ ( ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )
85 78 84 sylan ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )
86 76 85 syl ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )