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

Theorem fsplitfpar 7843
Description: Merge two functions with a common argument in parallel. Combination of fsplit 7841 and fpar 7840. (Contributed by AV, 3-Jan-2024.)
Hypotheses
Ref Expression
fsplitfpar.h 𝐻 = (((1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ ((2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))
fsplitfpar.s 𝑆 = ((1st ↾ I ) ↾ 𝐴)
Assertion
Ref Expression
fsplitfpar ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻𝑆) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺
Allowed substitution hints:   𝑆(𝑥)   𝐻(𝑥)

Proof of Theorem fsplitfpar
Dummy variables 𝑎 𝑝 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsplitfpar.s . . . . . . . . . 10 𝑆 = ((1st ↾ I ) ↾ 𝐴)
2 fsplit 7841 . . . . . . . . . . 11 (1st ↾ I ) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)
32reseq1i 5822 . . . . . . . . . 10 ((1st ↾ I ) ↾ 𝐴) = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)
41, 3eqtri 2762 . . . . . . . . 9 𝑆 = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)
54fveq1i 6678 . . . . . . . 8 (𝑆𝑎) = (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎)
65a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑆𝑎) = (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎))
7 fvres 6696 . . . . . . . . 9 (𝑎𝐴 → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)‘𝑎))
8 eqidd 2740 . . . . . . . . . 10 (𝑎𝐴 → (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩))
9 id 22 . . . . . . . . . . . 12 (𝑥 = 𝑎𝑥 = 𝑎)
109, 9opeq12d 4770 . . . . . . . . . . 11 (𝑥 = 𝑎 → ⟨𝑥, 𝑥⟩ = ⟨𝑎, 𝑎⟩)
1110adantl 485 . . . . . . . . . 10 ((𝑎𝐴𝑥 = 𝑎) → ⟨𝑥, 𝑥⟩ = ⟨𝑎, 𝑎⟩)
12 elex 3417 . . . . . . . . . 10 (𝑎𝐴𝑎 ∈ V)
13 opex 5323 . . . . . . . . . . 11 𝑎, 𝑎⟩ ∈ V
1413a1i 11 . . . . . . . . . 10 (𝑎𝐴 → ⟨𝑎, 𝑎⟩ ∈ V)
158, 11, 12, 14fvmptd 6785 . . . . . . . . 9 (𝑎𝐴 → ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)‘𝑎) = ⟨𝑎, 𝑎⟩)
167, 15eqtrd 2774 . . . . . . . 8 (𝑎𝐴 → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ⟨𝑎, 𝑎⟩)
1716adantl 485 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ⟨𝑎, 𝑎⟩)
186, 17eqtrd 2774 . . . . . 6 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑆𝑎) = ⟨𝑎, 𝑎⟩)
1918fveq2d 6681 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘(𝑆𝑎)) = (𝐻‘⟨𝑎, 𝑎⟩))
20 df-ov 7176 . . . . . 6 (𝑎𝐻𝑎) = (𝐻‘⟨𝑎, 𝑎⟩)
21 fsplitfpar.h . . . . . . . . 9 𝐻 = (((1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ ((2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))
2221fpar 7840 . . . . . . . 8 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝐻 = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩))
2322adantr 484 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → 𝐻 = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩))
24 fveq2 6677 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝐹𝑥) = (𝐹𝑎))
2524adantr 484 . . . . . . . . 9 ((𝑥 = 𝑎𝑦 = 𝑎) → (𝐹𝑥) = (𝐹𝑎))
26 fveq2 6677 . . . . . . . . . 10 (𝑦 = 𝑎 → (𝐺𝑦) = (𝐺𝑎))
2726adantl 485 . . . . . . . . 9 ((𝑥 = 𝑎𝑦 = 𝑎) → (𝐺𝑦) = (𝐺𝑎))
2825, 27opeq12d 4770 . . . . . . . 8 ((𝑥 = 𝑎𝑦 = 𝑎) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
2928adantl 485 . . . . . . 7 ((((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) ∧ (𝑥 = 𝑎𝑦 = 𝑎)) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
30 simpr 488 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → 𝑎𝐴)
31 opex 5323 . . . . . . . 8 ⟨(𝐹𝑎), (𝐺𝑎)⟩ ∈ V
3231a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ⟨(𝐹𝑎), (𝐺𝑎)⟩ ∈ V)
3323, 29, 30, 30, 32ovmpod 7320 . . . . . 6 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑎𝐻𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
3420, 33eqtr3id 2788 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘⟨𝑎, 𝑎⟩) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
3519, 34eqtrd 2774 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘(𝑆𝑎)) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
36 eqid 2739 . . . . . . . . . 10 (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) = (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩)
3736fnmpt 6478 . . . . . . . . 9 (∀𝑎 ∈ V ⟨𝑎, 𝑎⟩ ∈ V → (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V)
3813a1i 11 . . . . . . . . 9 (𝑎 ∈ V → ⟨𝑎, 𝑎⟩ ∈ V)
3937, 38mprg 3068 . . . . . . . 8 (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V
40 ssv 3902 . . . . . . . 8 𝐴 ⊆ V
41 fnssres 6460 . . . . . . . 8 (((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V ∧ 𝐴 ⊆ V) → ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
4239, 40, 41mp2an 692 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴
43 fsplit 7841 . . . . . . . . . 10 (1st ↾ I ) = (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩)
4443reseq1i 5822 . . . . . . . . 9 ((1st ↾ I ) ↾ 𝐴) = ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
451, 44eqtri 2762 . . . . . . . 8 𝑆 = ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
4645fneq1i 6436 . . . . . . 7 (𝑆 Fn 𝐴 ↔ ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
4742, 46mpbir 234 . . . . . 6 𝑆 Fn 𝐴
4847a1i 11 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝑆 Fn 𝐴)
49 fvco2 6768 . . . . 5 ((𝑆 Fn 𝐴𝑎𝐴) → ((𝐻𝑆)‘𝑎) = (𝐻‘(𝑆𝑎)))
5048, 49sylan 583 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝐻𝑆)‘𝑎) = (𝐻‘(𝑆𝑎)))
51 fveq2 6677 . . . . . . 7 (𝑥 = 𝑎 → (𝐺𝑥) = (𝐺𝑎))
5224, 51opeq12d 4770 . . . . . 6 (𝑥 = 𝑎 → ⟨(𝐹𝑥), (𝐺𝑥)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
53 eqid 2739 . . . . . 6 (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
5452, 53, 31fvmpt 6778 . . . . 5 (𝑎𝐴 → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
5554adantl 485 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
5635, 50, 553eqtr4d 2784 . . 3 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎))
5756ralrimiva 3097 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑎𝐴 ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎))
58 opex 5323 . . . . . . . 8 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
5958a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ (𝑥𝐴𝑦𝐴)) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V)
6059ralrimivva 3104 . . . . . 6 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑥𝐴𝑦𝐴 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V)
61 eqid 2739 . . . . . . 7 (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
6261fnmpo 7795 . . . . . 6 (∀𝑥𝐴𝑦𝐴 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V → (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴))
6360, 62syl 17 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴))
6422fneq1d 6432 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻 Fn (𝐴 × 𝐴) ↔ (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴)))
6563, 64mpbird 260 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝐻 Fn (𝐴 × 𝐴))
6613a1i 11 . . . . . . . 8 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎 ∈ V) → ⟨𝑎, 𝑎⟩ ∈ V)
6766ralrimiva 3097 . . . . . . 7 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑎 ∈ V ⟨𝑎, 𝑎⟩ ∈ V)
6867, 37syl 17 . . . . . 6 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V)
6968, 40, 41sylancl 589 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
7069, 46sylibr 237 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝑆 Fn 𝐴)
7145rneqi 5781 . . . . . 6 ran 𝑆 = ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
72 mptima 5916 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) “ 𝐴) = ran (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩)
73 df-ima 5539 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) “ 𝐴) = ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
74 eqid 2739 . . . . . . . 8 (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩) = (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩)
7574rnmpt 5799 . . . . . . 7 ran (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩) = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
7672, 73, 753eqtr3i 2770 . . . . . 6 ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
7771, 76eqtri 2762 . . . . 5 ran 𝑆 = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
78 elinel2 4087 . . . . . . . . 9 (𝑎 ∈ (V ∩ 𝐴) → 𝑎𝐴)
79 simpl 486 . . . . . . . . . . . 12 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → 𝑎𝐴)
8079, 79opelxpd 5564 . . . . . . . . . . 11 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴))
81 eleq1 2821 . . . . . . . . . . . 12 (𝑝 = ⟨𝑎, 𝑎⟩ → (𝑝 ∈ (𝐴 × 𝐴) ↔ ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴)))
8281adantl 485 . . . . . . . . . . 11 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → (𝑝 ∈ (𝐴 × 𝐴) ↔ ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴)))
8380, 82mpbird 260 . . . . . . . . . 10 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → 𝑝 ∈ (𝐴 × 𝐴))
8483ex 416 . . . . . . . . 9 (𝑎𝐴 → (𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴)))
8578, 84syl 17 . . . . . . . 8 (𝑎 ∈ (V ∩ 𝐴) → (𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴)))
8685rexlimiv 3191 . . . . . . 7 (∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴))
8786abssi 3960 . . . . . 6 {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩} ⊆ (𝐴 × 𝐴)
8887a1i 11 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩} ⊆ (𝐴 × 𝐴))
8977, 88eqsstrid 3926 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ran 𝑆 ⊆ (𝐴 × 𝐴))
90 fnco 6454 . . . 4 ((𝐻 Fn (𝐴 × 𝐴) ∧ 𝑆 Fn 𝐴 ∧ ran 𝑆 ⊆ (𝐴 × 𝐴)) → (𝐻𝑆) Fn 𝐴)
9165, 70, 89, 90syl3anc 1372 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻𝑆) Fn 𝐴)
92 opex 5323 . . . . . 6 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V
9392a1i 11 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑥𝐴) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V)
9493ralrimiva 3097 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V)
9553fnmpt 6478 . . . 4 (∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
9694, 95syl 17 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
97 eqfnfv 6812 . . 3 (((𝐻𝑆) Fn 𝐴 ∧ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴) → ((𝐻𝑆) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ↔ ∀𝑎𝐴 ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎)))
9891, 96, 97syl2anc 587 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ((𝐻𝑆) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ↔ ∀𝑎𝐴 ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎)))
9957, 98mpbird 260 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻𝑆) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wcel 2114  {cab 2717  wral 3054  wrex 3055  Vcvv 3399  cin 3843  wss 3844  cop 4523  cmpt 5111   I cid 5429   × cxp 5524  ccnv 5525  ran crn 5527  cres 5528  cima 5529  ccom 5530   Fn wfn 6335  cfv 6340  (class class class)co 7173  cmpo 7175  1st c1st 7715  2nd c2nd 7716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297  ax-un 7482
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-ov 7176  df-oprab 7177  df-mpo 7178  df-1st 7717  df-2nd 7718
This theorem is referenced by:  offsplitfpar  7844
  Copyright terms: Public domain W3C validator