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

Theorem fsplitfpar 7959
Description: Merge two functions with a common argument in parallel. Combination of fsplit 7957 and fpar 7956. (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 7957 . . . . . . . . . . 11 (1st ↾ I ) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)
32reseq1i 5887 . . . . . . . . . 10 ((1st ↾ I ) ↾ 𝐴) = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)
41, 3eqtri 2766 . . . . . . . . 9 𝑆 = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)
54fveq1i 6775 . . . . . . . 8 (𝑆𝑎) = (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎)
65a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑆𝑎) = (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎))
7 fvres 6793 . . . . . . . . 9 (𝑎𝐴 → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)‘𝑎))
8 eqidd 2739 . . . . . . . . . 10 (𝑎𝐴 → (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩))
9 id 22 . . . . . . . . . . . 12 (𝑥 = 𝑎𝑥 = 𝑎)
109, 9opeq12d 4812 . . . . . . . . . . 11 (𝑥 = 𝑎 → ⟨𝑥, 𝑥⟩ = ⟨𝑎, 𝑎⟩)
1110adantl 482 . . . . . . . . . 10 ((𝑎𝐴𝑥 = 𝑎) → ⟨𝑥, 𝑥⟩ = ⟨𝑎, 𝑎⟩)
12 elex 3450 . . . . . . . . . 10 (𝑎𝐴𝑎 ∈ V)
13 opex 5379 . . . . . . . . . . 11 𝑎, 𝑎⟩ ∈ V
1413a1i 11 . . . . . . . . . 10 (𝑎𝐴 → ⟨𝑎, 𝑎⟩ ∈ V)
158, 11, 12, 14fvmptd 6882 . . . . . . . . 9 (𝑎𝐴 → ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)‘𝑎) = ⟨𝑎, 𝑎⟩)
167, 15eqtrd 2778 . . . . . . . 8 (𝑎𝐴 → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ⟨𝑎, 𝑎⟩)
1716adantl 482 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ⟨𝑎, 𝑎⟩)
186, 17eqtrd 2778 . . . . . 6 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑆𝑎) = ⟨𝑎, 𝑎⟩)
1918fveq2d 6778 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘(𝑆𝑎)) = (𝐻‘⟨𝑎, 𝑎⟩))
20 df-ov 7278 . . . . . 6 (𝑎𝐻𝑎) = (𝐻‘⟨𝑎, 𝑎⟩)
21 fsplitfpar.h . . . . . . . . 9 𝐻 = (((1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ ((2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))
2221fpar 7956 . . . . . . . 8 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝐻 = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩))
2322adantr 481 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → 𝐻 = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩))
24 fveq2 6774 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝐹𝑥) = (𝐹𝑎))
2524adantr 481 . . . . . . . . 9 ((𝑥 = 𝑎𝑦 = 𝑎) → (𝐹𝑥) = (𝐹𝑎))
26 fveq2 6774 . . . . . . . . . 10 (𝑦 = 𝑎 → (𝐺𝑦) = (𝐺𝑎))
2726adantl 482 . . . . . . . . 9 ((𝑥 = 𝑎𝑦 = 𝑎) → (𝐺𝑦) = (𝐺𝑎))
2825, 27opeq12d 4812 . . . . . . . 8 ((𝑥 = 𝑎𝑦 = 𝑎) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
2928adantl 482 . . . . . . 7 ((((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) ∧ (𝑥 = 𝑎𝑦 = 𝑎)) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
30 simpr 485 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → 𝑎𝐴)
31 opex 5379 . . . . . . . 8 ⟨(𝐹𝑎), (𝐺𝑎)⟩ ∈ V
3231a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ⟨(𝐹𝑎), (𝐺𝑎)⟩ ∈ V)
3323, 29, 30, 30, 32ovmpod 7425 . . . . . 6 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑎𝐻𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
3420, 33eqtr3id 2792 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘⟨𝑎, 𝑎⟩) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
3519, 34eqtrd 2778 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘(𝑆𝑎)) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
36 eqid 2738 . . . . . . . . . 10 (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) = (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩)
3736fnmpt 6573 . . . . . . . . 9 (∀𝑎 ∈ V ⟨𝑎, 𝑎⟩ ∈ V → (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V)
3813a1i 11 . . . . . . . . 9 (𝑎 ∈ V → ⟨𝑎, 𝑎⟩ ∈ V)
3937, 38mprg 3078 . . . . . . . 8 (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V
40 ssv 3945 . . . . . . . 8 𝐴 ⊆ V
41 fnssres 6555 . . . . . . . 8 (((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V ∧ 𝐴 ⊆ V) → ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
4239, 40, 41mp2an 689 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴
43 fsplit 7957 . . . . . . . . . 10 (1st ↾ I ) = (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩)
4443reseq1i 5887 . . . . . . . . 9 ((1st ↾ I ) ↾ 𝐴) = ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
451, 44eqtri 2766 . . . . . . . 8 𝑆 = ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
4645fneq1i 6530 . . . . . . 7 (𝑆 Fn 𝐴 ↔ ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
4742, 46mpbir 230 . . . . . 6 𝑆 Fn 𝐴
4847a1i 11 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝑆 Fn 𝐴)
49 fvco2 6865 . . . . 5 ((𝑆 Fn 𝐴𝑎𝐴) → ((𝐻𝑆)‘𝑎) = (𝐻‘(𝑆𝑎)))
5048, 49sylan 580 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝐻𝑆)‘𝑎) = (𝐻‘(𝑆𝑎)))
51 fveq2 6774 . . . . . . 7 (𝑥 = 𝑎 → (𝐺𝑥) = (𝐺𝑎))
5224, 51opeq12d 4812 . . . . . 6 (𝑥 = 𝑎 → ⟨(𝐹𝑥), (𝐺𝑥)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
53 eqid 2738 . . . . . 6 (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
5452, 53, 31fvmpt 6875 . . . . 5 (𝑎𝐴 → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
5554adantl 482 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
5635, 50, 553eqtr4d 2788 . . 3 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎))
5756ralrimiva 3103 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑎𝐴 ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎))
58 opex 5379 . . . . . . . 8 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
5958a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ (𝑥𝐴𝑦𝐴)) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V)
6059ralrimivva 3123 . . . . . 6 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑥𝐴𝑦𝐴 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V)
61 eqid 2738 . . . . . . 7 (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
6261fnmpo 7909 . . . . . 6 (∀𝑥𝐴𝑦𝐴 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V → (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴))
6360, 62syl 17 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴))
6422fneq1d 6526 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻 Fn (𝐴 × 𝐴) ↔ (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴)))
6563, 64mpbird 256 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝐻 Fn (𝐴 × 𝐴))
6613a1i 11 . . . . . . . 8 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎 ∈ V) → ⟨𝑎, 𝑎⟩ ∈ V)
6766ralrimiva 3103 . . . . . . 7 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑎 ∈ V ⟨𝑎, 𝑎⟩ ∈ V)
6867, 37syl 17 . . . . . 6 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V)
6968, 40, 41sylancl 586 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
7069, 46sylibr 233 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝑆 Fn 𝐴)
7145rneqi 5846 . . . . . 6 ran 𝑆 = ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
72 mptima 5981 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) “ 𝐴) = ran (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩)
73 df-ima 5602 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) “ 𝐴) = ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
74 eqid 2738 . . . . . . . 8 (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩) = (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩)
7574rnmpt 5864 . . . . . . 7 ran (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩) = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
7672, 73, 753eqtr3i 2774 . . . . . 6 ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
7771, 76eqtri 2766 . . . . 5 ran 𝑆 = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
78 elinel2 4130 . . . . . . . . 9 (𝑎 ∈ (V ∩ 𝐴) → 𝑎𝐴)
79 simpl 483 . . . . . . . . . . . 12 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → 𝑎𝐴)
8079, 79opelxpd 5627 . . . . . . . . . . 11 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴))
81 eleq1 2826 . . . . . . . . . . . 12 (𝑝 = ⟨𝑎, 𝑎⟩ → (𝑝 ∈ (𝐴 × 𝐴) ↔ ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴)))
8281adantl 482 . . . . . . . . . . 11 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → (𝑝 ∈ (𝐴 × 𝐴) ↔ ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴)))
8380, 82mpbird 256 . . . . . . . . . 10 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → 𝑝 ∈ (𝐴 × 𝐴))
8483ex 413 . . . . . . . . 9 (𝑎𝐴 → (𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴)))
8578, 84syl 17 . . . . . . . 8 (𝑎 ∈ (V ∩ 𝐴) → (𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴)))
8685rexlimiv 3209 . . . . . . 7 (∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴))
8786abssi 4003 . . . . . 6 {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩} ⊆ (𝐴 × 𝐴)
8887a1i 11 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩} ⊆ (𝐴 × 𝐴))
8977, 88eqsstrid 3969 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ran 𝑆 ⊆ (𝐴 × 𝐴))
90 fnco 6549 . . . 4 ((𝐻 Fn (𝐴 × 𝐴) ∧ 𝑆 Fn 𝐴 ∧ ran 𝑆 ⊆ (𝐴 × 𝐴)) → (𝐻𝑆) Fn 𝐴)
9165, 70, 89, 90syl3anc 1370 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻𝑆) Fn 𝐴)
92 opex 5379 . . . . . 6 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V
9392a1i 11 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑥𝐴) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V)
9493ralrimiva 3103 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V)
9553fnmpt 6573 . . . 4 (∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
9694, 95syl 17 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
97 eqfnfv 6909 . . 3 (((𝐻𝑆) Fn 𝐴 ∧ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴) → ((𝐻𝑆) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ↔ ∀𝑎𝐴 ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎)))
9891, 96, 97syl2anc 584 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ((𝐻𝑆) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ↔ ∀𝑎𝐴 ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎)))
9957, 98mpbird 256 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻𝑆) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  {cab 2715  wral 3064  wrex 3065  Vcvv 3432  cin 3886  wss 3887  cop 4567  cmpt 5157   I cid 5488   × cxp 5587  ccnv 5588  ran crn 5590  cres 5591  cima 5592  ccom 5593   Fn wfn 6428  cfv 6433  (class class class)co 7275  cmpo 7277  1st c1st 7829  2nd c2nd 7830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832
This theorem is referenced by:  offsplitfpar  7960
  Copyright terms: Public domain W3C validator