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

 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.e ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
imasaddflem.a (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
Assertion
Ref Expression
imasaddfnlem (𝜑 Fn (𝐵 × 𝐵))
Distinct variable groups:   𝑞,𝑝,𝐵   𝑎,𝑏,𝑝,𝑞,𝑉   · ,𝑝,𝑞   𝐹,𝑎,𝑏,𝑝,𝑞   𝜑,𝑎,𝑏,𝑝,𝑞   ,𝑎,𝑏,𝑝,𝑞
Allowed substitution hints:   𝐵(𝑎,𝑏)   · (𝑎,𝑏)

Dummy variables 𝑤 𝑦 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 5060 . . . . . . . . 9 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ V
2 fvex 6342 . . . . . . . . 9 (𝐹‘(𝑝 · 𝑞)) ∈ V
31, 2relsnop 5367 . . . . . . . 8 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
43rgenw 3073 . . . . . . 7 𝑞𝑉 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
5 reliun 5378 . . . . . . 7 (Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑞𝑉 Rel {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
64, 5mpbir 221 . . . . . 6 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
76rgenw 3073 . . . . 5 𝑝𝑉 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
8 reliun 5378 . . . . 5 (Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∀𝑝𝑉 Rel 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
97, 8mpbir 221 . . . 4 Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}
10 imasaddflem.a . . . . 5 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
1110releqd 5343 . . . 4 (𝜑 → (Rel ↔ Rel 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
129, 11mpbiri 248 . . 3 (𝜑 → Rel )
13 imasaddf.f . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑉onto𝐵)
14 fof 6256 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
1513, 14syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑉𝐵)
16 ffvelrn 6500 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝑉𝐵𝑝𝑉) → (𝐹𝑝) ∈ 𝐵)
17 ffvelrn 6500 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝑉𝐵𝑞𝑉) → (𝐹𝑞) ∈ 𝐵)
1816, 17anim12dan 605 . . . . . . . . . . . . . . . . 17 ((𝐹:𝑉𝐵 ∧ (𝑝𝑉𝑞𝑉)) → ((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵))
1915, 18sylan 569 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵))
20 opelxpi 5288 . . . . . . . . . . . . . . . 16 (((𝐹𝑝) ∈ 𝐵 ∧ (𝐹𝑞) ∈ 𝐵) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵))
2119, 20syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵))
22 opelxpi 5288 . . . . . . . . . . . . . . 15 ((⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ (𝐵 × 𝐵) ∧ (𝐹‘(𝑝 · 𝑞)) ∈ V) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
2321, 2, 22sylancl 574 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ((𝐵 × 𝐵) × V))
2423snssd 4475 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑝𝑉𝑞𝑉)) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2524anassrs 458 . . . . . . . . . . . 12 (((𝜑𝑝𝑉) ∧ 𝑞𝑉) → {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2625ralrimiva 3115 . . . . . . . . . . 11 ((𝜑𝑝𝑉) → ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
27 iunss 4695 . . . . . . . . . . 11 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V) ↔ ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2826, 27sylibr 224 . . . . . . . . . 10 ((𝜑𝑝𝑉) → 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
2928ralrimiva 3115 . . . . . . . . 9 (𝜑 → ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
30 iunss 4695 . . . . . . . . 9 ( 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V) ↔ ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
3129, 30sylibr 224 . . . . . . . 8 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ((𝐵 × 𝐵) × V))
3210, 31eqsstrd 3788 . . . . . . 7 (𝜑 ⊆ ((𝐵 × 𝐵) × V))
33 dmss 5461 . . . . . . 7 ( ⊆ ((𝐵 × 𝐵) × V) → dom ⊆ dom ((𝐵 × 𝐵) × V))
3432, 33syl 17 . . . . . 6 (𝜑 → dom ⊆ dom ((𝐵 × 𝐵) × V))
35 vn0 4072 . . . . . . 7 V ≠ ∅
36 dmxp 5482 . . . . . . 7 (V ≠ ∅ → dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵))
3735, 36ax-mp 5 . . . . . 6 dom ((𝐵 × 𝐵) × V) = (𝐵 × 𝐵)
3834, 37syl6sseq 3800 . . . . 5 (𝜑 → dom ⊆ (𝐵 × 𝐵))
39 forn 6259 . . . . . . 7 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
4013, 39syl 17 . . . . . 6 (𝜑 → ran 𝐹 = 𝐵)
4140sqxpeqd 5281 . . . . 5 (𝜑 → (ran 𝐹 × ran 𝐹) = (𝐵 × 𝐵))
4238, 41sseqtr4d 3791 . . . 4 (𝜑 → dom ⊆ (ran 𝐹 × ran 𝐹))
4310eleq2d 2836 . . . . . . . . . . . . 13 (𝜑 → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
4443adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
45 df-br 4787 . . . . . . . . . . . 12 (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤 ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ )
46 eliun 4658 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
47 eliun 4658 . . . . . . . . . . . . . 14 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
4847rexbii 3189 . . . . . . . . . . . . 13 (∃𝑝𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
4946, 48bitr2i 265 . . . . . . . . . . . 12 (∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
5044, 45, 493bitr4g 303 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤 ↔ ∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩}))
51 opex 5060 . . . . . . . . . . . . . . 15 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ V
5251elsn 4331 . . . . . . . . . . . . . 14 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ↔ ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩)
53 opex 5060 . . . . . . . . . . . . . . . 16 ⟨(𝐹𝑎), (𝐹𝑏)⟩ ∈ V
54 vex 3354 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
5553, 54opth 5072 . . . . . . . . . . . . . . 15 (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ↔ (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
56 fvex 6342 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑎) ∈ V
57 fvex 6342 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑏) ∈ V
5856, 57opth 5072 . . . . . . . . . . . . . . . . . 18 (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ↔ ((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)))
59 imasaddf.e . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (((𝐹𝑎) = (𝐹𝑝) ∧ (𝐹𝑏) = (𝐹𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
6058, 59syl5bi 232 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))
61 eqeq2 2782 . . . . . . . . . . . . . . . . . 18 ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑎 · 𝑏)) ↔ 𝑤 = (𝐹‘(𝑝 · 𝑞))))
6261biimprd 238 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)) → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6360, 62syl6 35 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ → (𝑤 = (𝐹‘(𝑝 · 𝑞)) → 𝑤 = (𝐹‘(𝑎 · 𝑏)))))
6463impd 396 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → ((⟨(𝐹𝑎), (𝐹𝑏)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∧ 𝑤 = (𝐹‘(𝑝 · 𝑞))) → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6555, 64syl5bi 232 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6652, 65syl5bi 232 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑉𝑏𝑉) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
67663expa 1111 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑉𝑏𝑉)) ∧ (𝑝𝑉𝑞𝑉)) → (⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6867rexlimdvva 3186 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (∃𝑝𝑉𝑞𝑉 ⟨⟨(𝐹𝑎), (𝐹𝑏)⟩, 𝑤⟩ ∈ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑤 = (𝐹‘(𝑎 · 𝑏))))
6950, 68sylbid 230 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))))
7069alrimiv 2007 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → ∀𝑤(⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))))
71 mo2icl 3537 . . . . . . . . 9 (∀𝑤(⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤𝑤 = (𝐹‘(𝑎 · 𝑏))) → ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
7270, 71syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
7372ralrimivva 3120 . . . . . . 7 (𝜑 → ∀𝑎𝑉𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤)
74 fofn 6258 . . . . . . . . . 10 (𝐹:𝑉onto𝐵𝐹 Fn 𝑉)
7513, 74syl 17 . . . . . . . . 9 (𝜑𝐹 Fn 𝑉)
76 opeq2 4540 . . . . . . . . . . . 12 (𝑧 = (𝐹𝑏) → ⟨(𝐹𝑎), 𝑧⟩ = ⟨(𝐹𝑎), (𝐹𝑏)⟩)
7776breq1d 4796 . . . . . . . . . . 11 (𝑧 = (𝐹𝑏) → (⟨(𝐹𝑎), 𝑧 𝑤 ↔ ⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7877mobidv 2639 . . . . . . . . . 10 (𝑧 = (𝐹𝑏) → (∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
7978ralrn 6505 . . . . . . . . 9 (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
8075, 79syl 17 . . . . . . . 8 (𝜑 → (∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
8180ralbidv 3135 . . . . . . 7 (𝜑 → (∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤 ↔ ∀𝑎𝑉𝑏𝑉 ∃*𝑤⟨(𝐹𝑎), (𝐹𝑏)⟩ 𝑤))
8273, 81mpbird 247 . . . . . 6 (𝜑 → ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤)
83 opeq1 4539 . . . . . . . . . . 11 (𝑦 = (𝐹𝑎) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹𝑎), 𝑧⟩)
8483breq1d 4796 . . . . . . . . . 10 (𝑦 = (𝐹𝑎) → (⟨𝑦, 𝑧 𝑤 ↔ ⟨(𝐹𝑎), 𝑧 𝑤))
8584mobidv 2639 . . . . . . . . 9 (𝑦 = (𝐹𝑎) → (∃*𝑤𝑦, 𝑧 𝑤 ↔ ∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8685ralbidv 3135 . . . . . . . 8 (𝑦 = (𝐹𝑎) → (∀𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8786ralrn 6505 . . . . . . 7 (𝐹 Fn 𝑉 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8875, 87syl 17 . . . . . 6 (𝜑 → (∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤 ↔ ∀𝑎𝑉𝑧 ∈ ran 𝐹∃*𝑤⟨(𝐹𝑎), 𝑧 𝑤))
8982, 88mpbird 247 . . . . 5 (𝜑 → ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤)
90 breq1 4789 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 𝑤 ↔ ⟨𝑦, 𝑧 𝑤))
9190mobidv 2639 . . . . . 6 (𝑥 = ⟨𝑦, 𝑧⟩ → (∃*𝑤 𝑥 𝑤 ↔ ∃*𝑤𝑦, 𝑧 𝑤))
9291ralxp 5402 . . . . 5 (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤 ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹∃*𝑤𝑦, 𝑧 𝑤)
9389, 92sylibr 224 . . . 4 (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤)
94 ssralv 3815 . . . 4 (dom ⊆ (ran 𝐹 × ran 𝐹) → (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)∃*𝑤 𝑥 𝑤 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
9542, 93, 94sylc 65 . . 3 (𝜑 → ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤)
96 dffun7 6058 . . 3 (Fun ↔ (Rel ∧ ∀𝑥 ∈ dom ∃*𝑤 𝑥 𝑤))
9712, 95, 96sylanbrc 572 . 2 (𝜑 → Fun )
98 eqimss2 3807 . . . . . . . . . . 11 ( = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} → 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
9910, 98syl 17 . . . . . . . . . 10 (𝜑 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
100 iunss 4695 . . . . . . . . . 10 ( 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ↔ ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
10199, 100sylib 208 . . . . . . . . 9 (𝜑 → ∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
102 iunss 4695 . . . . . . . . . . 11 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ ↔ ∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
103 opex 5060 . . . . . . . . . . . . . 14 ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ V
104103snss 4451 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ ↔ {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ )
1051, 2opeldm 5466 . . . . . . . . . . . . 13 (⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩ ∈ → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
106104, 105sylbir 225 . . . . . . . . . . . 12 ({⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
107106ralimi 3101 . . . . . . . . . . 11 (∀𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
108102, 107sylbi 207 . . . . . . . . . 10 ( 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
109108ralimi 3101 . . . . . . . . 9 (∀𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩} ⊆ → ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
110101, 109syl 17 . . . . . . . 8 (𝜑 → ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom )
111 opeq2 4540 . . . . . . . . . . . 12 (𝑧 = (𝐹𝑞) → ⟨(𝐹𝑝), 𝑧⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
112111eleq1d 2835 . . . . . . . . . . 11 (𝑧 = (𝐹𝑞) → (⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
113112ralrn 6505 . . . . . . . . . 10 (𝐹 Fn 𝑉 → (∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
11475, 113syl 17 . . . . . . . . 9 (𝜑 → (∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
115114ralbidv 3135 . . . . . . . 8 (𝜑 → (∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ↔ ∀𝑝𝑉𝑞𝑉 ⟨(𝐹𝑝), (𝐹𝑞)⟩ ∈ dom ))
116110, 115mpbird 247 . . . . . . 7 (𝜑 → ∀𝑝𝑉𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom )
117 opeq1 4539 . . . . . . . . . . 11 (𝑦 = (𝐹𝑝) → ⟨𝑦, 𝑧⟩ = ⟨(𝐹𝑝), 𝑧⟩)
118117eleq1d 2835 . . . . . . . . . 10 (𝑦 = (𝐹𝑝) → (⟨𝑦, 𝑧⟩ ∈ dom ↔ ⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
119118ralbidv 3135 . . . . . . . . 9 (𝑦 = (𝐹𝑝) → (∀𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom ↔ ∀𝑧 ∈ ran 𝐹⟨(𝐹𝑝), 𝑧⟩ ∈ dom ))
120119ralrn 6505 . . . . . . . 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 2838 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑧⟩ → (𝑥 ∈ dom ↔ ⟨𝑦, 𝑧⟩ ∈ dom ))
124123ralxp 5402 . . . . . 6 (∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom ↔ ∀𝑦 ∈ ran 𝐹𝑧 ∈ ran 𝐹𝑦, 𝑧⟩ ∈ dom )
125122, 124sylibr 224 . . . . 5 (𝜑 → ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom )
126 dfss3 3741 . . . . 5 ((ran 𝐹 × ran 𝐹) ⊆ dom ↔ ∀𝑥 ∈ (ran 𝐹 × ran 𝐹)𝑥 ∈ dom )
127125, 126sylibr 224 . . . 4 (𝜑 → (ran 𝐹 × ran 𝐹) ⊆ dom )
12841, 127eqsstr3d 3789 . . 3 (𝜑 → (𝐵 × 𝐵) ⊆ dom )
12938, 128eqssd 3769 . 2 (𝜑 → dom = (𝐵 × 𝐵))
130 df-fn 6034 . 2 ( Fn (𝐵 × 𝐵) ↔ (Fun ∧ dom = (𝐵 × 𝐵)))
13197, 129, 130sylanbrc 572 1 (𝜑 Fn (𝐵 × 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071  ∀wal 1629   = wceq 1631   ∈ wcel 2145  ∃*wmo 2619   ≠ wne 2943  ∀wral 3061  ∃wrex 3062  Vcvv 3351   ⊆ wss 3723  ∅c0 4063  {csn 4316  ⟨cop 4322  ∪ ciun 4654   class class class wbr 4786   × cxp 5247  dom cdm 5249  ran crn 5250  Rel wrel 5254  Fun wfun 6025   Fn wfn 6026  ⟶wf 6027  –onto→wfo 6029  ‘cfv 6031  (class class class)co 6793 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fo 6037  df-fv 6039 This theorem is referenced by:  imasaddvallem  16397  imasaddflem  16398  imasaddfn  16399  imasmulfn  16402
 Copyright terms: Public domain W3C validator