MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tz7.48lem Structured version   Visualization version   GIF version

Theorem tz7.48lem 8479
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.
StepHypRef Expression
1 r2al 3192 . . . . . . 7 (∀𝑥𝐴𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)))
2 simpl 482 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴) → 𝑥𝐴)
32anim1i 615 . . . . . . . . . 10 (((𝑥𝐴𝑦𝐴) ∧ 𝑦𝑥) → (𝑥𝐴𝑦𝑥))
43imim1i 63 . . . . . . . . 9 (((𝑥𝐴𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)) → (((𝑥𝐴𝑦𝐴) ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)))
54expd 415 . . . . . . . 8 (((𝑥𝐴𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)) → ((𝑥𝐴𝑦𝐴) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
652alimi 1808 . . . . . . 7 (∀𝑥𝑦((𝑥𝐴𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)) → ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
71, 6sylbi 217 . . . . . 6 (∀𝑥𝐴𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
8 r2al 3192 . . . . . 6 (∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
97, 8sylibr 234 . . . . 5 (∀𝑥𝐴𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → ∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))
10 elequ1 2112 . . . . . . . . . . . 12 (𝑦 = 𝑤 → (𝑦𝑥𝑤𝑥))
11 fveq2 6906 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝐹𝑦) = (𝐹𝑤))
1211eqeq2d 2745 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → ((𝐹𝑥) = (𝐹𝑦) ↔ (𝐹𝑥) = (𝐹𝑤)))
1312notbid 318 . . . . . . . . . . . 12 (𝑦 = 𝑤 → (¬ (𝐹𝑥) = (𝐹𝑦) ↔ ¬ (𝐹𝑥) = (𝐹𝑤)))
1410, 13imbi12d 344 . . . . . . . . . . 11 (𝑦 = 𝑤 → ((𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) ↔ (𝑤𝑥 → ¬ (𝐹𝑥) = (𝐹𝑤))))
1514cbvralvw 3234 . . . . . . . . . 10 (∀𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) ↔ ∀𝑤𝐴 (𝑤𝑥 → ¬ (𝐹𝑥) = (𝐹𝑤)))
1615ralbii 3090 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) ↔ ∀𝑥𝐴𝑤𝐴 (𝑤𝑥 → ¬ (𝐹𝑥) = (𝐹𝑤)))
17 elequ2 2120 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑤𝑥𝑤𝑧))
18 fveqeq2 6915 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝐹𝑥) = (𝐹𝑤) ↔ (𝐹𝑧) = (𝐹𝑤)))
1918notbid 318 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (¬ (𝐹𝑥) = (𝐹𝑤) ↔ ¬ (𝐹𝑧) = (𝐹𝑤)))
2017, 19imbi12d 344 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((𝑤𝑥 → ¬ (𝐹𝑥) = (𝐹𝑤)) ↔ (𝑤𝑧 → ¬ (𝐹𝑧) = (𝐹𝑤))))
2120ralbidv 3175 . . . . . . . . . 10 (𝑥 = 𝑧 → (∀𝑤𝐴 (𝑤𝑥 → ¬ (𝐹𝑥) = (𝐹𝑤)) ↔ ∀𝑤𝐴 (𝑤𝑧 → ¬ (𝐹𝑧) = (𝐹𝑤))))
2221cbvralvw 3234 . . . . . . . . 9 (∀𝑥𝐴𝑤𝐴 (𝑤𝑥 → ¬ (𝐹𝑥) = (𝐹𝑤)) ↔ ∀𝑧𝐴𝑤𝐴 (𝑤𝑧 → ¬ (𝐹𝑧) = (𝐹𝑤)))
23 elequ1 2112 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤𝑧𝑥𝑧))
24 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
2524eqeq2d 2745 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → ((𝐹𝑧) = (𝐹𝑤) ↔ (𝐹𝑧) = (𝐹𝑥)))
2625notbid 318 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (¬ (𝐹𝑧) = (𝐹𝑤) ↔ ¬ (𝐹𝑧) = (𝐹𝑥)))
2723, 26imbi12d 344 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑤𝑧 → ¬ (𝐹𝑧) = (𝐹𝑤)) ↔ (𝑥𝑧 → ¬ (𝐹𝑧) = (𝐹𝑥))))
2827cbvralvw 3234 . . . . . . . . . . 11 (∀𝑤𝐴 (𝑤𝑧 → ¬ (𝐹𝑧) = (𝐹𝑤)) ↔ ∀𝑥𝐴 (𝑥𝑧 → ¬ (𝐹𝑧) = (𝐹𝑥)))
2928ralbii 3090 . . . . . . . . . 10 (∀𝑧𝐴𝑤𝐴 (𝑤𝑧 → ¬ (𝐹𝑧) = (𝐹𝑤)) ↔ ∀𝑧𝐴𝑥𝐴 (𝑥𝑧 → ¬ (𝐹𝑧) = (𝐹𝑥)))
30 elequ2 2120 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑥𝑧𝑥𝑦))
31 fveqeq2 6915 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐹𝑧) = (𝐹𝑥) ↔ (𝐹𝑦) = (𝐹𝑥)))
3231notbid 318 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (¬ (𝐹𝑧) = (𝐹𝑥) ↔ ¬ (𝐹𝑦) = (𝐹𝑥)))
3330, 32imbi12d 344 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ((𝑥𝑧 → ¬ (𝐹𝑧) = (𝐹𝑥)) ↔ (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥))))
3433ralbidv 3175 . . . . . . . . . . 11 (𝑧 = 𝑦 → (∀𝑥𝐴 (𝑥𝑧 → ¬ (𝐹𝑧) = (𝐹𝑥)) ↔ ∀𝑥𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥))))
3534cbvralvw 3234 . . . . . . . . . 10 (∀𝑧𝐴𝑥𝐴 (𝑥𝑧 → ¬ (𝐹𝑧) = (𝐹𝑥)) ↔ ∀𝑦𝐴𝑥𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)))
3629, 35bitri 275 . . . . . . . . 9 (∀𝑧𝐴𝑤𝐴 (𝑤𝑧 → ¬ (𝐹𝑧) = (𝐹𝑤)) ↔ ∀𝑦𝐴𝑥𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)))
3716, 22, 363bitri 297 . . . . . . . 8 (∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) ↔ ∀𝑦𝐴𝑥𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)))
38 ralcom 3286 . . . . . . . . 9 (∀𝑦𝐴𝑥𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)))
3938biimpi 216 . . . . . . . 8 (∀𝑦𝐴𝑥𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)))
4037, 39sylbi 217 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)))
4140ancri 549 . . . . . 6 (∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ ∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
42 r19.26-2 3135 . . . . . 6 (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) ↔ (∀𝑥𝐴𝑦𝐴 (𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ ∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
4341, 42sylibr 234 . . . . 5 (∀𝑥𝐴𝑦𝐴 (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)) → ∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
449, 43syl 17 . . . 4 (∀𝑥𝐴𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → ∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))
45 fvres 6925 . . . . . . . . . . 11 (𝑥𝐴 → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
46 fvres 6925 . . . . . . . . . . 11 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
4745, 46eqeqan12d 2748 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴) → (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) ↔ (𝐹𝑥) = (𝐹𝑦)))
4847ad2antrl 728 . . . . . . . . 9 ((𝐴 ⊆ On ∧ ((𝑥𝐴𝑦𝐴) ∧ ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))) → (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) ↔ (𝐹𝑥) = (𝐹𝑦)))
49 ssel 3988 . . . . . . . . . . . 12 (𝐴 ⊆ On → (𝑥𝐴𝑥 ∈ On))
50 ssel 3988 . . . . . . . . . . . 12 (𝐴 ⊆ On → (𝑦𝐴𝑦 ∈ On))
5149, 50anim12d 609 . . . . . . . . . . 11 (𝐴 ⊆ On → ((𝑥𝐴𝑦𝐴) → (𝑥 ∈ On ∧ 𝑦 ∈ On)))
52 pm3.48 965 . . . . . . . . . . . . . 14 (((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) → ((𝑥𝑦𝑦𝑥) → (¬ (𝐹𝑦) = (𝐹𝑥) ∨ ¬ (𝐹𝑥) = (𝐹𝑦))))
53 oridm 904 . . . . . . . . . . . . . . 15 ((¬ (𝐹𝑥) = (𝐹𝑦) ∨ ¬ (𝐹𝑥) = (𝐹𝑦)) ↔ ¬ (𝐹𝑥) = (𝐹𝑦))
54 eqcom 2741 . . . . . . . . . . . . . . . . 17 ((𝐹𝑥) = (𝐹𝑦) ↔ (𝐹𝑦) = (𝐹𝑥))
5554notbii 320 . . . . . . . . . . . . . . . 16 (¬ (𝐹𝑥) = (𝐹𝑦) ↔ ¬ (𝐹𝑦) = (𝐹𝑥))
5655orbi1i 913 . . . . . . . . . . . . . . 15 ((¬ (𝐹𝑥) = (𝐹𝑦) ∨ ¬ (𝐹𝑥) = (𝐹𝑦)) ↔ (¬ (𝐹𝑦) = (𝐹𝑥) ∨ ¬ (𝐹𝑥) = (𝐹𝑦)))
5753, 56bitr3i 277 . . . . . . . . . . . . . 14 (¬ (𝐹𝑥) = (𝐹𝑦) ↔ (¬ (𝐹𝑦) = (𝐹𝑥) ∨ ¬ (𝐹𝑥) = (𝐹𝑦)))
5852, 57imbitrrdi 252 . . . . . . . . . . . . 13 (((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) → ((𝑥𝑦𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)))
5958con2d 134 . . . . . . . . . . . 12 (((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) → ((𝐹𝑥) = (𝐹𝑦) → ¬ (𝑥𝑦𝑦𝑥)))
60 eloni 6395 . . . . . . . . . . . . 13 (𝑥 ∈ On → Ord 𝑥)
61 eloni 6395 . . . . . . . . . . . . 13 (𝑦 ∈ On → Ord 𝑦)
62 ordtri3 6421 . . . . . . . . . . . . . 14 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 = 𝑦 ↔ ¬ (𝑥𝑦𝑦𝑥)))
6362biimprd 248 . . . . . . . . . . . . 13 ((Ord 𝑥 ∧ Ord 𝑦) → (¬ (𝑥𝑦𝑦𝑥) → 𝑥 = 𝑦))
6460, 61, 63syl2an 596 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (¬ (𝑥𝑦𝑦𝑥) → 𝑥 = 𝑦))
6559, 64syl9r 78 . . . . . . . . . . 11 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
6651, 65syl6 35 . . . . . . . . . 10 (𝐴 ⊆ On → ((𝑥𝐴𝑦𝐴) → (((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
6766imp32 418 . . . . . . . . 9 ((𝐴 ⊆ On ∧ ((𝑥𝐴𝑦𝐴) ∧ ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
6848, 67sylbid 240 . . . . . . . 8 ((𝐴 ⊆ On ∧ ((𝑥𝐴𝑦𝐴) ∧ ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))) → (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦))
6968exp32 420 . . . . . . 7 (𝐴 ⊆ On → ((𝑥𝐴𝑦𝐴) → (((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) → (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦))))
7069a2d 29 . . . . . 6 (𝐴 ⊆ On → (((𝑥𝐴𝑦𝐴) → ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))) → ((𝑥𝐴𝑦𝐴) → (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦))))
71702alimdv 1915 . . . . 5 (𝐴 ⊆ On → (∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))) → ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦))))
72 r2al 3192 . . . . 5 (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))))
73 r2al 3192 . . . . 5 (∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)))
7471, 72, 733imtr4g 296 . . . 4 (𝐴 ⊆ On → (∀𝑥𝐴𝑦𝐴 ((𝑥𝑦 → ¬ (𝐹𝑦) = (𝐹𝑥)) ∧ (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))) → ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)))
7544, 74syl5 34 . . 3 (𝐴 ⊆ On → (∀𝑥𝐴𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)))
7675imdistani 568 . 2 ((𝐴 ⊆ On ∧ ∀𝑥𝐴𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦)) → (𝐴 ⊆ On ∧ ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)))
77 tz7.48.1 . . . 4 𝐹 Fn On
78 fnssres 6691 . . . 4 ((𝐹 Fn On ∧ 𝐴 ⊆ On) → (𝐹𝐴) Fn 𝐴)
7977, 78mpan 690 . . 3 (𝐴 ⊆ On → (𝐹𝐴) Fn 𝐴)
80 dffn2 6738 . . . 4 ((𝐹𝐴) Fn 𝐴 ↔ (𝐹𝐴):𝐴⟶V)
81 dff13 7274 . . . . . 6 ((𝐹𝐴):𝐴1-1→V ↔ ((𝐹𝐴):𝐴⟶V ∧ ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)))
82 df-f1 6567 . . . . . 6 ((𝐹𝐴):𝐴1-1→V ↔ ((𝐹𝐴):𝐴⟶V ∧ Fun (𝐹𝐴)))
8381, 82bitr3i 277 . . . . 5 (((𝐹𝐴):𝐴⟶V ∧ ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)) ↔ ((𝐹𝐴):𝐴⟶V ∧ Fun (𝐹𝐴)))
8483simprbi 496 . . . 4 (((𝐹𝐴):𝐴⟶V ∧ ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun (𝐹𝐴))
8580, 84sylanb 581 . . 3 (((𝐹𝐴) Fn 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun (𝐹𝐴))
8679, 85sylan 580 . 2 ((𝐴 ⊆ On ∧ ∀𝑥𝐴𝑦𝐴 (((𝐹𝐴)‘𝑥) = ((𝐹𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun (𝐹𝐴))
8776, 86syl 17 1 ((𝐴 ⊆ On ∧ ∀𝑥𝐴𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦)) → Fun (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  wal 1534   = wceq 1536  wcel 2105  wral 3058  Vcvv 3477  wss 3962  ccnv 5687  cres 5690  Ord word 6384  Oncon0 6385  Fun wfun 6556   Fn wfn 6557  wf 6558  1-1wf1 6559  cfv 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-res 5700  df-ord 6388  df-on 6389  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fv 6570
This theorem is referenced by:  tz7.48-2  8480  tz7.49  8483  zorn2lem4  10536
  Copyright terms: Public domain W3C validator