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

Theorem f1o2ndf1 7270
Description: The 2nd (second member of an ordered pair) function restricted to a one-to-one function 𝐹 is a one-to-one function of 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.)
Assertion
Ref Expression
f1o2ndf1 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹1-1-onto→ran 𝐹)

Proof of Theorem f1o2ndf1
Dummy variables 𝑎 𝑏 𝑣 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1f 6088 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fo2ndf 7269 . . 3 (𝐹:𝐴𝐵 → (2nd𝐹):𝐹onto→ran 𝐹)
31, 2syl 17 . 2 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹onto→ran 𝐹)
4 f2ndf 7268 . . . . 5 (𝐹:𝐴𝐵 → (2nd𝐹):𝐹𝐵)
51, 4syl 17 . . . 4 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹𝐵)
6 fssxp 6047 . . . . . . 7 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
71, 6syl 17 . . . . . 6 (𝐹:𝐴1-1𝐵𝐹 ⊆ (𝐴 × 𝐵))
8 ssel2 3590 . . . . . . . . . . 11 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝐹) → 𝑥 ∈ (𝐴 × 𝐵))
9 elxp2 5122 . . . . . . . . . . 11 (𝑥 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩)
108, 9sylib 208 . . . . . . . . . 10 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝐹) → ∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩)
11 ssel2 3590 . . . . . . . . . . 11 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑦𝐹) → 𝑦 ∈ (𝐴 × 𝐵))
12 elxp2 5122 . . . . . . . . . . 11 (𝑦 ∈ (𝐴 × 𝐵) ↔ ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩)
1311, 12sylib 208 . . . . . . . . . 10 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑦𝐹) → ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩)
1410, 13anim12dan 881 . . . . . . . . 9 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩ ∧ ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩))
15 fvres 6194 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑎, 𝑣⟩ ∈ 𝐹 → ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑎, 𝑣⟩))
1615adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑎, 𝑣⟩))
1716adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑎, 𝑣⟩))
18 fvres 6194 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑏, 𝑤⟩ ∈ 𝐹 → ((2nd𝐹)‘⟨𝑏, 𝑤⟩) = (2nd ‘⟨𝑏, 𝑤⟩))
1918ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((2nd𝐹)‘⟨𝑏, 𝑤⟩) = (2nd ‘⟨𝑏, 𝑤⟩))
2017, 19eqeq12d 2635 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) ↔ (2nd ‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑏, 𝑤⟩)))
21 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎 ∈ V
22 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑣 ∈ V
2321, 22op2nd 7162 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ‘⟨𝑎, 𝑣⟩) = 𝑣
24 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏 ∈ V
25 vex 3198 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤 ∈ V
2624, 25op2nd 7162 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ‘⟨𝑏, 𝑤⟩) = 𝑤
2723, 26eqeq12i 2634 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑏, 𝑤⟩) ↔ 𝑣 = 𝑤)
28 f1fun 6090 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
29 funopfv 6222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Fun 𝐹 → (⟨𝑎, 𝑣⟩ ∈ 𝐹 → (𝐹𝑎) = 𝑣))
30 funopfv 6222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Fun 𝐹 → (⟨𝑏, 𝑤⟩ ∈ 𝐹 → (𝐹𝑏) = 𝑤))
3129, 30anim12d 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝐹 → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → ((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤)))
3228, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐴1-1𝐵 → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → ((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤)))
33 eqcom 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐹𝑎) = 𝑣𝑣 = (𝐹𝑎))
3433biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹𝑎) = 𝑣𝑣 = (𝐹𝑎))
35 eqcom 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐹𝑏) = 𝑤𝑤 = (𝐹𝑏))
3635biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹𝑏) = 𝑤𝑤 = (𝐹𝑏))
3734, 36eqeqan12d 2636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝑣 = 𝑤 ↔ (𝐹𝑎) = (𝐹𝑏)))
38 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝐴𝑣𝐵) → 𝑎𝐴)
39 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑏𝐴𝑤𝐵) → 𝑏𝐴)
4038, 39anim12i 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑎𝐴𝑏𝐴))
41 f1veqaeq 6499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐹:𝐴1-1𝐵 ∧ (𝑎𝐴𝑏𝐴)) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
4240, 41sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐹:𝐴1-1𝐵 ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
43 opeq12 4395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 = 𝑏𝑣 = 𝑤) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)
4443ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 𝑏 → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))
4542, 44syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐹:𝐴1-1𝐵 ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((𝐹𝑎) = (𝐹𝑏) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
4645com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐹:𝐴1-1𝐵 ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝑣 = 𝑤 → ((𝐹𝑎) = (𝐹𝑏) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
4746ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐹:𝐴1-1𝐵 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → ((𝐹𝑎) = (𝐹𝑏) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
4847com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐹𝑎) = (𝐹𝑏) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
4937, 48syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝑣 = 𝑤 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))))
5049com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑤 → (𝑣 = 𝑤 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))))
5150pm2.43i 52 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑤 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5251com14 96 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹:𝐴1-1𝐵 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5352com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐴1-1𝐵 → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5432, 53syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:𝐴1-1𝐵 → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5554com13 88 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → (𝐹:𝐴1-1𝐵 → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5655impcom 446 . . . . . . . . . . . . . . . . . . . . . . . 24 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝐹:𝐴1-1𝐵 → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
5756com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝑣 = 𝑤 → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
5827, 57syl5bi 232 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((2nd ‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑏, 𝑤⟩) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
5920, 58sylbid 230 . . . . . . . . . . . . . . . . . . . . 21 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
6059com23 86 . . . . . . . . . . . . . . . . . . . 20 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
6160ex 450 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6261adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6362com12 32 . . . . . . . . . . . . . . . . 17 (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6463adantlr 750 . . . . . . . . . . . . . . . 16 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6564adantr 481 . . . . . . . . . . . . . . 15 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
66 eleq1 2687 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑎, 𝑣⟩ → (𝑥𝐹 ↔ ⟨𝑎, 𝑣⟩ ∈ 𝐹))
6766ad2antlr 762 . . . . . . . . . . . . . . . . 17 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → (𝑥𝐹 ↔ ⟨𝑎, 𝑣⟩ ∈ 𝐹))
68 eleq1 2687 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑏, 𝑤⟩ → (𝑦𝐹 ↔ ⟨𝑏, 𝑤⟩ ∈ 𝐹))
6967, 68bi2anan9 916 . . . . . . . . . . . . . . . 16 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝑥𝐹𝑦𝐹) ↔ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)))
7069anbi2d 739 . . . . . . . . . . . . . . 15 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹))))
71 fveq2 6178 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨𝑎, 𝑣⟩ → ((2nd𝐹)‘𝑥) = ((2nd𝐹)‘⟨𝑎, 𝑣⟩))
7271ad2antlr 762 . . . . . . . . . . . . . . . . . 18 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → ((2nd𝐹)‘𝑥) = ((2nd𝐹)‘⟨𝑎, 𝑣⟩))
73 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑏, 𝑤⟩ → ((2nd𝐹)‘𝑦) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩))
7472, 73eqeqan12d 2636 . . . . . . . . . . . . . . . . 17 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) ↔ ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩)))
75 simpllr 798 . . . . . . . . . . . . . . . . . 18 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → 𝑥 = ⟨𝑎, 𝑣⟩)
76 simpr 477 . . . . . . . . . . . . . . . . . 18 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → 𝑦 = ⟨𝑏, 𝑤⟩)
7775, 76eqeq12d 2635 . . . . . . . . . . . . . . . . 17 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → (𝑥 = 𝑦 ↔ ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))
7874, 77imbi12d 334 . . . . . . . . . . . . . . . 16 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
7978imbi2d 330 . . . . . . . . . . . . . . 15 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)) ↔ (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
8065, 70, 793imtr4d 283 . . . . . . . . . . . . . 14 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
8180ex 450 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → (𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))))
8281rexlimdvva 3034 . . . . . . . . . . . 12 (((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) → (∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))))
8382ex 450 . . . . . . . . . . 11 ((𝑎𝐴𝑣𝐵) → (𝑥 = ⟨𝑎, 𝑣⟩ → (∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))))
8483rexlimivv 3032 . . . . . . . . . 10 (∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩ → (∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))))
8584imp 445 . . . . . . . . 9 ((∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩ ∧ ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
8614, 85mpcom 38 . . . . . . . 8 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))
8786ex 450 . . . . . . 7 (𝐹 ⊆ (𝐴 × 𝐵) → ((𝑥𝐹𝑦𝐹) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
8887com23 86 . . . . . 6 (𝐹 ⊆ (𝐴 × 𝐵) → (𝐹:𝐴1-1𝐵 → ((𝑥𝐹𝑦𝐹) → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
897, 88mpcom 38 . . . . 5 (𝐹:𝐴1-1𝐵 → ((𝑥𝐹𝑦𝐹) → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))
9089ralrimivv 2967 . . . 4 (𝐹:𝐴1-1𝐵 → ∀𝑥𝐹𝑦𝐹 (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))
91 dff13 6497 . . . 4 ((2nd𝐹):𝐹1-1𝐵 ↔ ((2nd𝐹):𝐹𝐵 ∧ ∀𝑥𝐹𝑦𝐹 (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))
925, 90, 91sylanbrc 697 . . 3 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹1-1𝐵)
93 df-f1 5881 . . . 4 ((2nd𝐹):𝐹1-1𝐵 ↔ ((2nd𝐹):𝐹𝐵 ∧ Fun (2nd𝐹)))
9493simprbi 480 . . 3 ((2nd𝐹):𝐹1-1𝐵 → Fun (2nd𝐹))
9592, 94syl 17 . 2 (𝐹:𝐴1-1𝐵 → Fun (2nd𝐹))
96 dff1o3 6130 . 2 ((2nd𝐹):𝐹1-1-onto→ran 𝐹 ↔ ((2nd𝐹):𝐹onto→ran 𝐹 ∧ Fun (2nd𝐹)))
973, 95, 96sylanbrc 697 1 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹1-1-onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wral 2909  wrex 2910  wss 3567  cop 4174   × cxp 5102  ccnv 5103  ran crn 5105  cres 5106  Fun wfun 5870  wf 5872  1-1wf1 5873  ontowfo 5874  1-1-ontowf1o 5875  cfv 5876  2nd c2nd 7152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-2nd 7154
This theorem is referenced by:  hashf1rn  13125  hashf1rnOLD  13126
  Copyright terms: Public domain W3C validator