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

Theorem imasaddfnlem 16116
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 4898 . . . . . . . . 9 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ V
2 fvex 6163 . . . . . . . . 9 (𝐹‘(𝑝 · 𝑞)) ∈ V
31, 2relsnop 5190 . . . . . . . 8 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
43rgenw 2919 . . . . . . 7 𝑞𝑉 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
5 reliun 5205 . . . . . . 7 (Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞𝑉 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
64, 5mpbir 221 . . . . . 6 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
76rgenw 2919 . . . . 5 𝑝𝑉 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
8 reliun 5205 . . . . 5 (Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝𝑉 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
97, 8mpbir 221 . . . 4 Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
10 imasaddflem.a . . . . 5 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
1110releqd 5169 . . . 4 (𝜑 → (Rel ↔ Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
129, 11mpbiri 248 . . 3 (𝜑 → Rel )
13 imasaddf.f . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑉onto𝐵)
14 fof 6077 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
1513, 14syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑉𝐵)
16 ffvelrn 6318 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝑉𝐵𝑝𝑉) → (𝐹𝑝) ∈ 𝐵)
17 ffvelrn 6318 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝑉𝐵𝑞𝑉) → (𝐹𝑞) ∈ 𝐵)
1816, 17anim12dan 881 . . . . . . . . . . . . . . . . 17 ((𝐹:𝑉𝐵 ∧ (𝑝𝑉𝑞𝑉)) → ((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵))
1915, 18sylan 488 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵))
20 opelxpi 5113 . . . . . . . . . . . . . . . 16 (((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵))
2119, 20syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵))
22 opelxpi 5113 . . . . . . . . . . . . . . 15 ((⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
2321, 2, 22sylancl 693 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
2423snssd 4314 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2524anassrs 679 . . . . . . . . . . . 12 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2625ralrimiva 2961 . . . . . . . . . . 11 ((𝜑𝑝𝑉) → ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
27 iunss 4532 . . . . . . . . . . 11 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V) ↔ ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2826, 27sylibr 224 . . . . . . . . . 10 ((𝜑𝑝𝑉) → 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2928ralrimiva 2961 . . . . . . . . 9 (𝜑 → ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
30 iunss 4532 . . . . . . . . 9 ( 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V) ↔ ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
3129, 30sylibr 224 . . . . . . . 8 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
3210, 31eqsstrd 3623 . . . . . . 7 (𝜑 ⊆ ((𝐵 × 𝐵) × V))
33 dmss 5288 . . . . . . 7 ( ⊆ ((𝐵 × 𝐵) × V) → dom ⊆ dom ((𝐵 × 𝐵) × V))
3432, 33syl 17 . . . . . 6 (𝜑 → dom ⊆ dom ((𝐵 × 𝐵) × V))
35 vn0 3905 . . . . . . 7 V ≠ ∅
36 dmxp 5309 . . . . . . 7 (V ≠ ∅ → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
3735, 36ax-mp 5 . . . . . 6 dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
3834, 37syl6sseq 3635 . . . . 5 (𝜑 → dom ⊆ (𝐵 × 𝐵))
39 forn 6080 . . . . . . 7 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
4013, 39syl 17 . . . . . 6 (𝜑 → ran 𝐹 = 𝐵)
4140sqxpeqd 5106 . . . . 5 (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
4238, 41sseqtr4d 3626 . . . 4 (𝜑 → dom ⊆ (ran 𝐹 × ran 𝐹))
4310eleq2d 2684 . . . . . . . . . . . . 13 (𝜑 → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
4443adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
45 df-br 4619 . . . . . . . . . . . 12 (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤 ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ )
46 eliun 4495 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
47 eliun 4495 . . . . . . . . . . . . . 14 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
4847rexbii 3035 . . . . . . . . . . . . 13 (∃𝑝𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
4946, 48bitr2i 265 . . . . . . . . . . . 12 (∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
5044, 45, 493bitr4g 303 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤 ↔ ∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
51 opex 4898 . . . . . . . . . . . . . . 15 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ V
5251elsn 4168 . . . . . . . . . . . . . 14 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩)
53 opex 4898 . . . . . . . . . . . . . . . 16 ⟨(𝐹𝑎), (𝐹𝑏)⟩ ∈ V
54 vex 3192 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
5553, 54opth 4910 . . . . . . . . . . . . . . 15 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
56 fvex 6163 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑎) ∈ V
57 fvex 6163 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑏) ∈ V
5856, 57opth 4910 . . . . . . . . . . . . . . . . . 18 (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ↔ ((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)))
59 imasaddf.e . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
6058, 59syl5bi 232 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
61 eqeq2 2632 . . . . . . . . . . . . . . . . . 18 ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
6261biimprd 238 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6360, 62syl6 35 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))))
6463impd 447 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → ((⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6555, 64syl5bi 232 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6652, 65syl5bi 232 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
67663expa 1262 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑉𝑏𝑉)) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6867rexlimdvva 3032 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6950, 68sylbid 230 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))))
7069alrimiv 1852 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → ∀𝑤(⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))))
71 mo2icl 3371 . . . . . . . . 9 (∀𝑤(⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
7270, 71syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
7372ralrimivva 2966 . . . . . . 7 (𝜑 → ∀𝑎𝑉𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
74 fofn 6079 . . . . . . . . . 10 (𝐹:𝑉onto𝐵𝐹 Fn 𝑉)
7513, 74syl 17 . . . . . . . . 9 (𝜑𝐹 Fn 𝑉)
76 opeq2 4376 . . . . . . . . . . . 12 (𝑧 = (𝐹𝑏) → ⟨(𝐹𝑎), 𝑧⟩ = ⟨(𝐹𝑎), (𝐹𝑏)⟩)
7776breq1d 4628 . . . . . . . . . . 11 (𝑧 = (𝐹𝑏) → (⟨(𝐹𝑎), 𝑧 𝑤 ↔ ⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7877mobidv 2490 . . . . . . . . . 10 (𝑧 = (𝐹𝑏) → (∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7978ralrn 6323 . . . . . . . . 9 (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
8075, 79syl 17 . . . . . . . 8 (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
8180ralbidv 2981 . . . . . . 7 (𝜑 → (∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑎𝑉𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
8273, 81mpbird 247 . . . . . 6 (𝜑 → ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤)
83 opeq1 4375 . . . . . . . . . . 11 (𝑦 = (𝐹𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹𝑎), 𝑧⟩)
8483breq1d 4628 . . . . . . . . . 10 (𝑦 = (𝐹𝑎) → (⟨𝑦, 𝑧 𝑤 ↔ ⟨(𝐹𝑎), 𝑧 𝑤))
8584mobidv 2490 . . . . . . . . 9 (𝑦 = (𝐹𝑎) → (∃*𝑤𝑦, 𝑧 𝑤 ↔ ∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8685ralbidv 2981 . . . . . . . 8 (𝑦 = (𝐹𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8786ralrn 6323 . . . . . . 7 (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8875, 87syl 17 . . . . . 6 (𝜑 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8982, 88mpbird 247 . . . . 5 (𝜑 → ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤)
90 breq1 4621 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 𝑤 ↔ ⟨𝑦, 𝑧 𝑤))
9190mobidv 2490 . . . . . 6 (𝑥 = ⟨𝑦, 𝑧⟩ → (∃*𝑤 𝑥 𝑤 ↔ ∃*𝑤𝑦, 𝑧 𝑤))
9291ralxp 5228 . . . . 5 (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤 ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤)
9389, 92sylibr 224 . . . 4 (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤)
94 ssralv 3650 . . . 4 (dom ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
9542, 93, 94sylc 65 . . 3 (𝜑 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤)
96 dffun7 5879 . . 3 (Fun ↔ (Rel ∧ ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
9712, 95, 96sylanbrc 697 . 2 (𝜑 → Fun )
98 eqimss2 3642 . . . . . . . . . . 11 ( = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
9910, 98syl 17 . . . . . . . . . 10 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
100 iunss 4532 . . . . . . . . . 10 ( 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ↔ ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
10199, 100sylib 208 . . . . . . . . 9 (𝜑 → ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
102 iunss 4532 . . . . . . . . . . 11 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ↔ ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
103 opex 4898 . . . . . . . . . . . . . 14 ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V
104103snss 4291 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ↔ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
1051, 2opeldm 5293 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
106104, 105sylbir 225 . . . . . . . . . . . 12 ({⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
107106ralimi 2947 . . . . . . . . . . 11 (∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
108102, 107sylbi 207 . . . . . . . . . 10 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
109108ralimi 2947 . . . . . . . . 9 (∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
110101, 109syl 17 . . . . . . . 8 (𝜑 → ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
111 opeq2 4376 . . . . . . . . . . . 12 (𝑧 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑧⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
112111eleq1d 2683 . . . . . . . . . . 11 (𝑧 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
113112ralrn 6323 . . . . . . . . . 10 (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
11475, 113syl 17 . . . . . . . . 9 (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
115114ralbidv 2981 . . . . . . . 8 (𝜑 → (∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
116110, 115mpbird 247 . . . . . . 7 (𝜑 → ∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom )
117 opeq1 4375 . . . . . . . . . . 11 (𝑦 = (𝐹𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹𝑝), 𝑧⟩)
118117eleq1d 2683 . . . . . . . . . 10 (𝑦 = (𝐹𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ↔ ⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
119118ralbidv 2981 . . . . . . . . 9 (𝑦 = (𝐹𝑝) → (∀𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
120119ralrn 6323 . . . . . . . 8 (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom ↔ ∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
12175, 120syl 17 . . . . . . 7 (𝜑 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom ↔ ∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
122116, 121mpbird 247 . . . . . 6 (𝜑 → ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom )
123 eleq1 2686 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ↔ ⟨𝑦, 𝑧⟩ ∈ dom ))
124123ralxp 5228 . . . . . 6 (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom )
125122, 124sylibr 224 . . . . 5 (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom )
126 dfss3 3577 . . . . 5 ((ran 𝐹 × ran 𝐹) ⊆ dom ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom )
127125, 126sylibr 224 . . . 4 (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom )
12841, 127eqsstr3d 3624 . . 3 (𝜑 → (𝐵 × 𝐵) ⊆ dom )
12938, 128eqssd 3604 . 2 (𝜑 → dom = (𝐵 × 𝐵))
130 df-fn 5855 . 2 ( Fn (𝐵 × 𝐵) ↔ (Fun ∧ dom = (𝐵 × 𝐵)))
13197, 129, 130sylanbrc 697 1 (𝜑 Fn (𝐵 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1478   = wceq 1480  wcel 1987  ∃*wmo 2470  wne 2790  wral 2907  wrex 2908  Vcvv 3189  wss 3559  c0 3896  {csn 4153  cop 4159   ciun 4490   class class class wbr 4618   × cxp 5077  dom cdm 5079  ran crn 5080  Rel wrel 5084  Fun wfun 5846   Fn wfn 5847  wf 5848  ontowfo 5850  cfv 5852  (class class class)co 6610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fo 5858  df-fv 5860
This theorem is referenced by:  imasaddvallem  16117  imasaddflem  16118  imasaddfn  16119  imasmulfn  16122
  Copyright terms: Public domain W3C validator