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

Theorem imasaddfnlem 17456
Description: The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)
Hypotheses
Ref Expression
imasaddf.f (𝜑𝐹:𝑉onto𝐵)
imasaddf.e ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
imasaddflem.a (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
Assertion
Ref Expression
imasaddfnlem (𝜑 Fn (𝐵 × 𝐵))
Distinct variable groups:   𝑞,𝑝,𝐵   𝑎,𝑏,𝑝,𝑞,𝑉   · ,𝑝,𝑞   𝐹,𝑎,𝑏,𝑝,𝑞   𝜑,𝑎,𝑏,𝑝,𝑞   ,𝑎,𝑏,𝑝,𝑞
Allowed substitution hints:   𝐵(𝑎,𝑏)   · (𝑎,𝑏)

Proof of Theorem imasaddfnlem
Dummy variables 𝑤 𝑦 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 5457 . . . . . . . . 9 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ V
2 fvex 6891 . . . . . . . . 9 (𝐹‘(𝑝 · 𝑞)) ∈ V
31, 2relsnop 5797 . . . . . . . 8 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
43rgenw 3064 . . . . . . 7 𝑞𝑉 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
5 reliun 5808 . . . . . . 7 (Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞𝑉 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
64, 5mpbir 230 . . . . . 6 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
76rgenw 3064 . . . . 5 𝑝𝑉 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
8 reliun 5808 . . . . 5 (Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝𝑉 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
97, 8mpbir 230 . . . 4 Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
10 imasaddflem.a . . . . 5 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
1110releqd 5770 . . . 4 (𝜑 → (Rel ↔ Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
129, 11mpbiri 257 . . 3 (𝜑 → Rel )
13 imasaddf.f . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑉onto𝐵)
14 fof 6792 . . . . . . . . . . . . . . . 16 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
1513, 14syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝑉𝐵)
16 ffvelcdm 7068 . . . . . . . . . . . . . . . 16 ((𝐹:𝑉𝐵𝑝𝑉) → (𝐹𝑝) ∈ 𝐵)
17 ffvelcdm 7068 . . . . . . . . . . . . . . . 16 ((𝐹:𝑉𝐵𝑞𝑉) → (𝐹𝑞) ∈ 𝐵)
1816, 17anim12dan 619 . . . . . . . . . . . . . . 15 ((𝐹:𝑉𝐵 ∧ (𝑝𝑉𝑞𝑉)) → ((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵))
1915, 18sylan 580 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵))
20 opelxpi 5706 . . . . . . . . . . . . . 14 (((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵))
2119, 20syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵))
22 opelxpi 5706 . . . . . . . . . . . . 13 ((⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
2321, 2, 22sylancl 586 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
2423snssd 4805 . . . . . . . . . . 11 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2524anassrs 468 . . . . . . . . . 10 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2625iunssd 5046 . . . . . . . . 9 ((𝜑𝑝𝑉) → 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2726iunssd 5046 . . . . . . . 8 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2810, 27eqsstrd 4016 . . . . . . 7 (𝜑 ⊆ ((𝐵 × 𝐵) × V))
29 dmss 5894 . . . . . . 7 ( ⊆ ((𝐵 × 𝐵) × V) → dom ⊆ dom ((𝐵 × 𝐵) × V))
3028, 29syl 17 . . . . . 6 (𝜑 → dom ⊆ dom ((𝐵 × 𝐵) × V))
31 vn0 4334 . . . . . . 7 V ≠ ∅
32 dmxp 5920 . . . . . . 7 (V ≠ ∅ → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
3331, 32ax-mp 5 . . . . . 6 dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
3430, 33sseqtrdi 4028 . . . . 5 (𝜑 → dom ⊆ (𝐵 × 𝐵))
35 forn 6795 . . . . . . 7 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
3613, 35syl 17 . . . . . 6 (𝜑 → ran 𝐹 = 𝐵)
3736sqxpeqd 5701 . . . . 5 (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
3834, 37sseqtrrd 4019 . . . 4 (𝜑 → dom ⊆ (ran 𝐹 × ran 𝐹))
3910eleq2d 2818 . . . . . . . . . . . . 13 (𝜑 → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
4039adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
41 df-br 5142 . . . . . . . . . . . 12 (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤 ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ )
42 eliun 4994 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
43 eliun 4994 . . . . . . . . . . . . . 14 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
4443rexbii 3093 . . . . . . . . . . . . 13 (∃𝑝𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
4542, 44bitr2i 275 . . . . . . . . . . . 12 (∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
4640, 41, 453bitr4g 313 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤 ↔ ∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
47 opex 5457 . . . . . . . . . . . . . . 15 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ V
4847elsn 4637 . . . . . . . . . . . . . 14 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩)
49 opex 5457 . . . . . . . . . . . . . . . 16 ⟨(𝐹𝑎), (𝐹𝑏)⟩ ∈ V
50 vex 3477 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
5149, 50opth 5469 . . . . . . . . . . . . . . 15 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
52 fvex 6891 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑎) ∈ V
53 fvex 6891 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑏) ∈ V
5452, 53opth 5469 . . . . . . . . . . . . . . . . . 18 (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ↔ ((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)))
55 imasaddf.e . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
5654, 55biimtrid 241 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
57 eqeq2 2743 . . . . . . . . . . . . . . . . . 18 ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
5857biimprd 247 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
5956, 58syl6 35 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))))
6059impd 411 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → ((⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6151, 60biimtrid 241 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6248, 61biimtrid 241 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
63623expa 1118 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑉𝑏𝑉)) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6463rexlimdvva 3210 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6546, 64sylbid 239 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))))
6665alrimiv 1930 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → ∀𝑤(⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))))
67 mo2icl 3706 . . . . . . . . 9 (∀𝑤(⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
6866, 67syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
6968ralrimivva 3199 . . . . . . 7 (𝜑 → ∀𝑎𝑉𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
70 fofn 6794 . . . . . . . . . 10 (𝐹:𝑉onto𝐵𝐹 Fn 𝑉)
7113, 70syl 17 . . . . . . . . 9 (𝜑𝐹 Fn 𝑉)
72 opeq2 4867 . . . . . . . . . . . 12 (𝑧 = (𝐹𝑏) → ⟨(𝐹𝑎), 𝑧⟩ = ⟨(𝐹𝑎), (𝐹𝑏)⟩)
7372breq1d 5151 . . . . . . . . . . 11 (𝑧 = (𝐹𝑏) → (⟨(𝐹𝑎), 𝑧 𝑤 ↔ ⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7473mobidv 2542 . . . . . . . . . 10 (𝑧 = (𝐹𝑏) → (∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7574ralrn 7074 . . . . . . . . 9 (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7671, 75syl 17 . . . . . . . 8 (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7776ralbidv 3176 . . . . . . 7 (𝜑 → (∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑎𝑉𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7869, 77mpbird 256 . . . . . 6 (𝜑 → ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤)
79 opeq1 4866 . . . . . . . . . . 11 (𝑦 = (𝐹𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹𝑎), 𝑧⟩)
8079breq1d 5151 . . . . . . . . . 10 (𝑦 = (𝐹𝑎) → (⟨𝑦, 𝑧 𝑤 ↔ ⟨(𝐹𝑎), 𝑧 𝑤))
8180mobidv 2542 . . . . . . . . 9 (𝑦 = (𝐹𝑎) → (∃*𝑤𝑦, 𝑧 𝑤 ↔ ∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8281ralbidv 3176 . . . . . . . 8 (𝑦 = (𝐹𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8382ralrn 7074 . . . . . . 7 (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8471, 83syl 17 . . . . . 6 (𝜑 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8578, 84mpbird 256 . . . . 5 (𝜑 → ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤)
86 breq1 5144 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 𝑤 ↔ ⟨𝑦, 𝑧 𝑤))
8786mobidv 2542 . . . . . 6 (𝑥 = ⟨𝑦, 𝑧⟩ → (∃*𝑤 𝑥 𝑤 ↔ ∃*𝑤𝑦, 𝑧 𝑤))
8887ralxp 5833 . . . . 5 (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤 ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤)
8985, 88sylibr 233 . . . 4 (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤)
90 ssralv 4046 . . . 4 (dom ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
9138, 89, 90sylc 65 . . 3 (𝜑 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤)
92 dffun7 6564 . . 3 (Fun ↔ (Rel ∧ ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
9312, 91, 92sylanbrc 583 . 2 (𝜑 → Fun )
94 eqimss2 4037 . . . . . . . . . . 11 ( = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
9510, 94syl 17 . . . . . . . . . 10 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
96 iunss 5041 . . . . . . . . . 10 ( 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ↔ ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
9795, 96sylib 217 . . . . . . . . 9 (𝜑 → ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
98 iunss 5041 . . . . . . . . . . 11 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ↔ ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
99 opex 5457 . . . . . . . . . . . . . 14 ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V
10099snss 4782 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ↔ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
1011, 2opeldm 5899 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
102100, 101sylbir 234 . . . . . . . . . . . 12 ({⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
103102ralimi 3082 . . . . . . . . . . 11 (∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
10498, 103sylbi 216 . . . . . . . . . 10 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
105104ralimi 3082 . . . . . . . . 9 (∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
10697, 105syl 17 . . . . . . . 8 (𝜑 → ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
107 opeq2 4867 . . . . . . . . . . . 12 (𝑧 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑧⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
108107eleq1d 2817 . . . . . . . . . . 11 (𝑧 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
109108ralrn 7074 . . . . . . . . . 10 (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
11071, 109syl 17 . . . . . . . . 9 (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
111110ralbidv 3176 . . . . . . . 8 (𝜑 → (∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
112106, 111mpbird 256 . . . . . . 7 (𝜑 → ∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom )
113 opeq1 4866 . . . . . . . . . . 11 (𝑦 = (𝐹𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹𝑝), 𝑧⟩)
114113eleq1d 2817 . . . . . . . . . 10 (𝑦 = (𝐹𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ↔ ⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
115114ralbidv 3176 . . . . . . . . 9 (𝑦 = (𝐹𝑝) → (∀𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
116115ralrn 7074 . . . . . . . 8 (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom ↔ ∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
11771, 116syl 17 . . . . . . 7 (𝜑 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom ↔ ∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
118112, 117mpbird 256 . . . . . 6 (𝜑 → ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom )
119 eleq1 2820 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ↔ ⟨𝑦, 𝑧⟩ ∈ dom ))
120119ralxp 5833 . . . . . 6 (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom )
121118, 120sylibr 233 . . . . 5 (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom )
122 dfss3 3966 . . . . 5 ((ran 𝐹 × ran 𝐹) ⊆ dom ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom )
123121, 122sylibr 233 . . . 4 (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom )
12437, 123eqsstrrd 4017 . . 3 (𝜑 → (𝐵 × 𝐵) ⊆ dom )
12534, 124eqssd 3995 . 2 (𝜑 → dom = (𝐵 × 𝐵))
126 df-fn 6535 . 2 ( Fn (𝐵 × 𝐵) ↔ (Fun ∧ dom = (𝐵 × 𝐵)))
12793, 125, 126sylanbrc 583 1 (𝜑 Fn (𝐵 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087  wal 1539   = wceq 1541  wcel 2106  ∃*wmo 2531  wne 2939  wral 3060  wrex 3069  Vcvv 3473  wss 3944  c0 4318  {csn 4622  cop 4628   ciun 4990   class class class wbr 5141   × cxp 5667  dom cdm 5669  ran crn 5670  Rel wrel 5674  Fun wfun 6526   Fn wfn 6527  wf 6528  ontowfo 6530  cfv 6532  (class class class)co 7393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-fo 6538  df-fv 6540
This theorem is referenced by:  imasaddvallem  17457  imasaddflem  17458  imasaddfn  17459  imasmulfn  17462
  Copyright terms: Public domain W3C validator