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

Theorem f1o2ndf1 7149
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 5999 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fo2ndf 7148 . . 3 (𝐹:𝐴𝐵 → (2nd𝐹):𝐹onto→ran 𝐹)
31, 2syl 17 . 2 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹onto→ran 𝐹)
4 f2ndf 7147 . . . . 5 (𝐹:𝐴𝐵 → (2nd𝐹):𝐹𝐵)
51, 4syl 17 . . . 4 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹𝐵)
6 fssxp 5959 . . . . . . 7 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
71, 6syl 17 . . . . . 6 (𝐹:𝐴1-1𝐵𝐹 ⊆ (𝐴 × 𝐵))
8 ssel2 3562 . . . . . . . . . . 11 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝐹) → 𝑥 ∈ (𝐴 × 𝐵))
9 elxp2 5046 . . . . . . . . . . 11 (𝑥 ∈ (𝐴 × 𝐵) ↔ ∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩)
108, 9sylib 206 . . . . . . . . . 10 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑥𝐹) → ∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩)
11 ssel2 3562 . . . . . . . . . . 11 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑦𝐹) → 𝑦 ∈ (𝐴 × 𝐵))
12 elxp2 5046 . . . . . . . . . . 11 (𝑦 ∈ (𝐴 × 𝐵) ↔ ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩)
1311, 12sylib 206 . . . . . . . . . 10 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ 𝑦𝐹) → ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩)
1410, 13anim12dan 877 . . . . . . . . 9 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩ ∧ ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩))
15 fvres 6102 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨𝑎, 𝑣⟩ ∈ 𝐹 → ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑎, 𝑣⟩))
1615adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑎, 𝑣⟩))
1716adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑎, 𝑣⟩))
18 fvres 6102 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑏, 𝑤⟩ ∈ 𝐹 → ((2nd𝐹)‘⟨𝑏, 𝑤⟩) = (2nd ‘⟨𝑏, 𝑤⟩))
1918ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((2nd𝐹)‘⟨𝑏, 𝑤⟩) = (2nd ‘⟨𝑏, 𝑤⟩))
2017, 19eqeq12d 2624 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) ↔ (2nd ‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑏, 𝑤⟩)))
21 vex 3175 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎 ∈ V
22 vex 3175 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑣 ∈ V
2321, 22op2nd 7045 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ‘⟨𝑎, 𝑣⟩) = 𝑣
24 vex 3175 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏 ∈ V
25 vex 3175 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤 ∈ V
2624, 25op2nd 7045 . . . . . . . . . . . . . . . . . . . . . . . 24 (2nd ‘⟨𝑏, 𝑤⟩) = 𝑤
2723, 26eqeq12i 2623 . . . . . . . . . . . . . . . . . . . . . . 23 ((2nd ‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑏, 𝑤⟩) ↔ 𝑣 = 𝑤)
28 f1fun 6001 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
29 funopfv 6130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Fun 𝐹 → (⟨𝑎, 𝑣⟩ ∈ 𝐹 → (𝐹𝑎) = 𝑣))
30 funopfv 6130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Fun 𝐹 → (⟨𝑏, 𝑤⟩ ∈ 𝐹 → (𝐹𝑏) = 𝑤))
3129, 30anim12d 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (Fun 𝐹 → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → ((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤)))
3228, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐴1-1𝐵 → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → ((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤)))
33 eqcom 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐹𝑎) = 𝑣𝑣 = (𝐹𝑎))
3433biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹𝑎) = 𝑣𝑣 = (𝐹𝑎))
35 eqcom 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐹𝑏) = 𝑤𝑤 = (𝐹𝑏))
3635biimpi 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐹𝑏) = 𝑤𝑤 = (𝐹𝑏))
3734, 36eqeqan12d 2625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝑣 = 𝑤 ↔ (𝐹𝑎) = (𝐹𝑏)))
38 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑎𝐴𝑣𝐵) → 𝑎𝐴)
39 simpl 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑏𝐴𝑤𝐵) → 𝑏𝐴)
4038, 39anim12i 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑎𝐴𝑏𝐴))
41 f1veqaeq 6396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐹:𝐴1-1𝐵 ∧ (𝑎𝐴𝑏𝐴)) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
4240, 41sylan2 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐹:𝐴1-1𝐵 ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((𝐹𝑎) = (𝐹𝑏) → 𝑎 = 𝑏))
43 opeq12 4336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑎 = 𝑏𝑣 = 𝑤) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)
4443ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = 𝑏 → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))
4542, 44syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐹:𝐴1-1𝐵 ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((𝐹𝑎) = (𝐹𝑏) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
4645com23 83 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐹:𝐴1-1𝐵 ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝑣 = 𝑤 → ((𝐹𝑎) = (𝐹𝑏) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
4746ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐹:𝐴1-1𝐵 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → ((𝐹𝑎) = (𝐹𝑏) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
4847com14 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐹𝑎) = (𝐹𝑏) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
4937, 48syl6bi 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝑣 = 𝑤 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))))
5049com14 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑣 = 𝑤 → (𝑣 = 𝑤 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))))
5150pm2.43i 49 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑣 = 𝑤 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5251com14 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹:𝐴1-1𝐵 → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5352com23 83 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐴1-1𝐵 → (((𝐹𝑎) = 𝑣 ∧ (𝐹𝑏) = 𝑤) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5432, 53syld 45 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:𝐴1-1𝐵 → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5554com13 85 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → (𝐹:𝐴1-1𝐵 → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
5655impcom 444 . . . . . . . . . . . . . . . . . . . . . . . 24 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝐹:𝐴1-1𝐵 → (𝑣 = 𝑤 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
5756com23 83 . . . . . . . . . . . . . . . . . . . . . . 23 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝑣 = 𝑤 → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
5827, 57syl5bi 230 . . . . . . . . . . . . . . . . . . . . . 22 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → ((2nd ‘⟨𝑎, 𝑣⟩) = (2nd ‘⟨𝑏, 𝑤⟩) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
5920, 58sylbid 228 . . . . . . . . . . . . . . . . . . . . 21 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → (𝐹:𝐴1-1𝐵 → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
6059com23 83 . . . . . . . . . . . . . . . . . . . 20 (((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) ∧ ((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵))) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
6160ex 448 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6261adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6362com12 32 . . . . . . . . . . . . . . . . 17 (((𝑎𝐴𝑣𝐵) ∧ (𝑏𝐴𝑤𝐵)) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6463adantlr 746 . . . . . . . . . . . . . . . 16 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
6564adantr 479 . . . . . . . . . . . . . . 15 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
66 eleq1 2675 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑎, 𝑣⟩ → (𝑥𝐹 ↔ ⟨𝑎, 𝑣⟩ ∈ 𝐹))
6766ad2antlr 758 . . . . . . . . . . . . . . . . 17 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → (𝑥𝐹 ↔ ⟨𝑎, 𝑣⟩ ∈ 𝐹))
68 eleq1 2675 . . . . . . . . . . . . . . . . 17 (𝑦 = ⟨𝑏, 𝑤⟩ → (𝑦𝐹 ↔ ⟨𝑏, 𝑤⟩ ∈ 𝐹))
6967, 68bi2anan9 912 . . . . . . . . . . . . . . . 16 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝑥𝐹𝑦𝐹) ↔ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹)))
7069anbi2d 735 . . . . . . . . . . . . . . 15 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ (⟨𝑎, 𝑣⟩ ∈ 𝐹 ∧ ⟨𝑏, 𝑤⟩ ∈ 𝐹))))
71 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑥 = ⟨𝑎, 𝑣⟩ → ((2nd𝐹)‘𝑥) = ((2nd𝐹)‘⟨𝑎, 𝑣⟩))
7271ad2antlr 758 . . . . . . . . . . . . . . . . . 18 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → ((2nd𝐹)‘𝑥) = ((2nd𝐹)‘⟨𝑎, 𝑣⟩))
73 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑦 = ⟨𝑏, 𝑤⟩ → ((2nd𝐹)‘𝑦) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩))
7472, 73eqeqan12d 2625 . . . . . . . . . . . . . . . . 17 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) ↔ ((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩)))
75 simpllr 794 . . . . . . . . . . . . . . . . . 18 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → 𝑥 = ⟨𝑎, 𝑣⟩)
76 simpr 475 . . . . . . . . . . . . . . . . . 18 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → 𝑦 = ⟨𝑏, 𝑤⟩)
7775, 76eqeq12d 2624 . . . . . . . . . . . . . . . . 17 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → (𝑥 = 𝑦 ↔ ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))
7874, 77imbi12d 332 . . . . . . . . . . . . . . . 16 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦) ↔ (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩)))
7978imbi2d 328 . . . . . . . . . . . . . . 15 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)) ↔ (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘⟨𝑎, 𝑣⟩) = ((2nd𝐹)‘⟨𝑏, 𝑤⟩) → ⟨𝑎, 𝑣⟩ = ⟨𝑏, 𝑤⟩))))
8065, 70, 793imtr4d 281 . . . . . . . . . . . . . 14 (((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) ∧ 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
8180ex 448 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) ∧ (𝑏𝐴𝑤𝐵)) → (𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))))
8281rexlimdvva 3019 . . . . . . . . . . . 12 (((𝑎𝐴𝑣𝐵) ∧ 𝑥 = ⟨𝑎, 𝑣⟩) → (∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))))
8382ex 448 . . . . . . . . . . 11 ((𝑎𝐴𝑣𝐵) → (𝑥 = ⟨𝑎, 𝑣⟩ → (∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))))
8483rexlimivv 3017 . . . . . . . . . 10 (∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩ → (∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩ → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))))
8584imp 443 . . . . . . . . 9 ((∃𝑎𝐴𝑣𝐵 𝑥 = ⟨𝑎, 𝑣⟩ ∧ ∃𝑏𝐴𝑤𝐵 𝑦 = ⟨𝑏, 𝑤⟩) → ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
8614, 85mpcom 37 . . . . . . . 8 ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥𝐹𝑦𝐹)) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))
8786ex 448 . . . . . . 7 (𝐹 ⊆ (𝐴 × 𝐵) → ((𝑥𝐹𝑦𝐹) → (𝐹:𝐴1-1𝐵 → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
8887com23 83 . . . . . 6 (𝐹 ⊆ (𝐴 × 𝐵) → (𝐹:𝐴1-1𝐵 → ((𝑥𝐹𝑦𝐹) → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))))
897, 88mpcom 37 . . . . 5 (𝐹:𝐴1-1𝐵 → ((𝑥𝐹𝑦𝐹) → (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))
9089ralrimivv 2952 . . . 4 (𝐹:𝐴1-1𝐵 → ∀𝑥𝐹𝑦𝐹 (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦))
91 dff13 6394 . . . 4 ((2nd𝐹):𝐹1-1𝐵 ↔ ((2nd𝐹):𝐹𝐵 ∧ ∀𝑥𝐹𝑦𝐹 (((2nd𝐹)‘𝑥) = ((2nd𝐹)‘𝑦) → 𝑥 = 𝑦)))
925, 90, 91sylanbrc 694 . . 3 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹1-1𝐵)
93 df-f1 5795 . . . 4 ((2nd𝐹):𝐹1-1𝐵 ↔ ((2nd𝐹):𝐹𝐵 ∧ Fun (2nd𝐹)))
9493simprbi 478 . . 3 ((2nd𝐹):𝐹1-1𝐵 → Fun (2nd𝐹))
9592, 94syl 17 . 2 (𝐹:𝐴1-1𝐵 → Fun (2nd𝐹))
96 dff1o3 6041 . 2 ((2nd𝐹):𝐹1-1-onto→ran 𝐹 ↔ ((2nd𝐹):𝐹onto→ran 𝐹 ∧ Fun (2nd𝐹)))
973, 95, 96sylanbrc 694 1 (𝐹:𝐴1-1𝐵 → (2nd𝐹):𝐹1-1-onto→ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  wrex 2896  wss 3539  cop 4130   × cxp 5026  ccnv 5027  ran crn 5029  cres 5030  Fun wfun 5784  wf 5786  1-1wf1 5787  ontowfo 5788  1-1-ontowf1o 5789  cfv 5790  2nd c2nd 7035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-2nd 7037
This theorem is referenced by:  hashf1rn  12956  hashf1rnOLD  12957
  Copyright terms: Public domain W3C validator