This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ralcom ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
40 39 biimpi ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
41 38 40 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
42 41 ancri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
43 r19.26-2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
44 42 43 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
45 10 44 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
46 fvres ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
47 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
48 46 47 eqeqan12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
49 48 ad2antrl ⊢ ( ( 𝐴 ⊆ On ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
50 ssel ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On ) )
51 ssel ⊢ ( 𝐴 ⊆ On → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On ) )
52 50 51 anim12d ⊢ ( 𝐴 ⊆ On → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) )
53 pm3.48 ⊢ ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ( ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
54 oridm ⊢ ( ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
55 eqcom ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
56 55 notbii ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
57 56 orbi1i ⊢ ( ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
58 54 57 bitr3i ⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∨ ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
59 53 58 imbitrrdi ⊢ ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
60 59 con2d ⊢ ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) )
61 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
62 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
63 ordtri3 ⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( 𝑥 = 𝑦 ↔ ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ) )
64 63 biimprd ⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → 𝑥 = 𝑦 ) )
65 61 62 64 syl2an ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ¬ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) → 𝑥 = 𝑦 ) )
66 60 65 syl9r ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
67 52 66 syl6 ⊢ ( 𝐴 ⊆ On → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
68 67 imp32 ⊢ ( ( 𝐴 ⊆ On ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
69 49 68 sylbid ⊢ ( ( 𝐴 ⊆ On ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
70 69 exp32 ⊢ ( 𝐴 ⊆ On → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
71 70 a2d ⊢ ( 𝐴 ⊆ On → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
72 71 2alimdv ⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
73 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) ) )
74 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
75 72 73 74 3imtr4g ⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∈ 𝑦 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑥 → ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
76 45 75 syl5 ⊢ ( 𝐴 ⊆ On → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
77 76 imdistani ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
78 fnssres ⊢ ( ( 𝐹 Fn On ∧ 𝐴 ⊆ On ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
79 1 78 mpan ⊢ ( 𝐴 ⊆ On → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
80 dffn2 ⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V )
81 dff13 ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ V ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
82 df-f1 ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1→ V ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ Fun ◡ ( 𝐹 ↾ 𝐴 ) ) )
83 81 82 bitr3i ⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ Fun ◡ ( 𝐹 ↾ 𝐴 ) ) )
84 83 simprbi ⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ V ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )
85 80 84 sylanb ⊢ ( ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )
86 79 85 sylan ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )
87 77 86 syl ⊢ ( ( 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ¬ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → Fun ◡ ( 𝐹 ↾ 𝐴 ) )