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

Theorem fsplitfpar 8050
Description: Merge two functions with a common argument in parallel. Combination of fsplit 8049 and fpar 8048. (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 8049 . . . . . . . . . . 11 (1st ↾ I ) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)
32reseq1i 5933 . . . . . . . . . 10 ((1st ↾ I ) ↾ 𝐴) = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)
41, 3eqtri 2764 . . . . . . . . 9 𝑆 = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)
54fveq1i 6843 . . . . . . . 8 (𝑆𝑎) = (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎)
65a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑆𝑎) = (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎))
7 fvres 6861 . . . . . . . . 9 (𝑎𝐴 → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)‘𝑎))
8 eqidd 2737 . . . . . . . . . 10 (𝑎𝐴 → (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) = (𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩))
9 id 22 . . . . . . . . . . . 12 (𝑥 = 𝑎𝑥 = 𝑎)
109, 9opeq12d 4838 . . . . . . . . . . 11 (𝑥 = 𝑎 → ⟨𝑥, 𝑥⟩ = ⟨𝑎, 𝑎⟩)
1110adantl 482 . . . . . . . . . 10 ((𝑎𝐴𝑥 = 𝑎) → ⟨𝑥, 𝑥⟩ = ⟨𝑎, 𝑎⟩)
12 elex 3463 . . . . . . . . . 10 (𝑎𝐴𝑎 ∈ V)
13 opex 5421 . . . . . . . . . . 11 𝑎, 𝑎⟩ ∈ V
1413a1i 11 . . . . . . . . . 10 (𝑎𝐴 → ⟨𝑎, 𝑎⟩ ∈ V)
158, 11, 12, 14fvmptd 6955 . . . . . . . . 9 (𝑎𝐴 → ((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩)‘𝑎) = ⟨𝑎, 𝑎⟩)
167, 15eqtrd 2776 . . . . . . . 8 (𝑎𝐴 → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ⟨𝑎, 𝑎⟩)
1716adantl 482 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (((𝑥 ∈ V ↦ ⟨𝑥, 𝑥⟩) ↾ 𝐴)‘𝑎) = ⟨𝑎, 𝑎⟩)
186, 17eqtrd 2776 . . . . . 6 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑆𝑎) = ⟨𝑎, 𝑎⟩)
1918fveq2d 6846 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘(𝑆𝑎)) = (𝐻‘⟨𝑎, 𝑎⟩))
20 df-ov 7360 . . . . . 6 (𝑎𝐻𝑎) = (𝐻‘⟨𝑎, 𝑎⟩)
21 fsplitfpar.h . . . . . . . . 9 𝐻 = (((1st ↾ (V × V)) ∘ (𝐹 ∘ (1st ↾ (V × V)))) ∩ ((2nd ↾ (V × V)) ∘ (𝐺 ∘ (2nd ↾ (V × V)))))
2221fpar 8048 . . . . . . . 8 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝐻 = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩))
2322adantr 481 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → 𝐻 = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩))
24 fveq2 6842 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝐹𝑥) = (𝐹𝑎))
2524adantr 481 . . . . . . . . 9 ((𝑥 = 𝑎𝑦 = 𝑎) → (𝐹𝑥) = (𝐹𝑎))
26 fveq2 6842 . . . . . . . . . 10 (𝑦 = 𝑎 → (𝐺𝑦) = (𝐺𝑎))
2726adantl 482 . . . . . . . . 9 ((𝑥 = 𝑎𝑦 = 𝑎) → (𝐺𝑦) = (𝐺𝑎))
2825, 27opeq12d 4838 . . . . . . . 8 ((𝑥 = 𝑎𝑦 = 𝑎) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
2928adantl 482 . . . . . . 7 ((((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) ∧ (𝑥 = 𝑎𝑦 = 𝑎)) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
30 simpr 485 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → 𝑎𝐴)
31 opex 5421 . . . . . . . 8 ⟨(𝐹𝑎), (𝐺𝑎)⟩ ∈ V
3231a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ⟨(𝐹𝑎), (𝐺𝑎)⟩ ∈ V)
3323, 29, 30, 30, 32ovmpod 7507 . . . . . 6 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝑎𝐻𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
3420, 33eqtr3id 2790 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘⟨𝑎, 𝑎⟩) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
3519, 34eqtrd 2776 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → (𝐻‘(𝑆𝑎)) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
36 eqid 2736 . . . . . . . . . 10 (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) = (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩)
3736fnmpt 6641 . . . . . . . . 9 (∀𝑎 ∈ V ⟨𝑎, 𝑎⟩ ∈ V → (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V)
3813a1i 11 . . . . . . . . 9 (𝑎 ∈ V → ⟨𝑎, 𝑎⟩ ∈ V)
3937, 38mprg 3070 . . . . . . . 8 (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V
40 ssv 3968 . . . . . . . 8 𝐴 ⊆ V
41 fnssres 6624 . . . . . . . 8 (((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) Fn V ∧ 𝐴 ⊆ V) → ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
4239, 40, 41mp2an 690 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴
43 fsplit 8049 . . . . . . . . . 10 (1st ↾ I ) = (𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩)
4443reseq1i 5933 . . . . . . . . 9 ((1st ↾ I ) ↾ 𝐴) = ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
451, 44eqtri 2764 . . . . . . . 8 𝑆 = ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
4645fneq1i 6599 . . . . . . 7 (𝑆 Fn 𝐴 ↔ ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) Fn 𝐴)
4742, 46mpbir 230 . . . . . 6 𝑆 Fn 𝐴
4847a1i 11 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝑆 Fn 𝐴)
49 fvco2 6938 . . . . 5 ((𝑆 Fn 𝐴𝑎𝐴) → ((𝐻𝑆)‘𝑎) = (𝐻‘(𝑆𝑎)))
5048, 49sylan 580 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝐻𝑆)‘𝑎) = (𝐻‘(𝑆𝑎)))
51 fveq2 6842 . . . . . . 7 (𝑥 = 𝑎 → (𝐺𝑥) = (𝐺𝑎))
5224, 51opeq12d 4838 . . . . . 6 (𝑥 = 𝑎 → ⟨(𝐹𝑥), (𝐺𝑥)⟩ = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
53 eqid 2736 . . . . . 6 (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
5452, 53, 31fvmpt 6948 . . . . 5 (𝑎𝐴 → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
5554adantl 482 . . . 4 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎) = ⟨(𝐹𝑎), (𝐺𝑎)⟩)
5635, 50, 553eqtr4d 2786 . . 3 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎𝐴) → ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎))
5756ralrimiva 3143 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑎𝐴 ((𝐻𝑆)‘𝑎) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑎))
58 opex 5421 . . . . . . . 8 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
5958a1i 11 . . . . . . 7 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ (𝑥𝐴𝑦𝐴)) → ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V)
6059ralrimivva 3197 . . . . . 6 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑥𝐴𝑦𝐴 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V)
61 eqid 2736 . . . . . . 7 (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) = (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
6261fnmpo 8001 . . . . . 6 (∀𝑥𝐴𝑦𝐴 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V → (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴))
6360, 62syl 17 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴))
6422fneq1d 6595 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻 Fn (𝐴 × 𝐴) ↔ (𝑥𝐴, 𝑦𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩) Fn (𝐴 × 𝐴)))
6563, 64mpbird 256 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → 𝐻 Fn (𝐴 × 𝐴))
6613a1i 11 . . . . . . . 8 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑎 ∈ V) → ⟨𝑎, 𝑎⟩ ∈ V)
6766ralrimiva 3143 . . . . . . 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 5892 . . . . . 6 ran 𝑆 = ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
72 mptima 6025 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) “ 𝐴) = ran (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩)
73 df-ima 5646 . . . . . . 7 ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) “ 𝐴) = ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴)
74 eqid 2736 . . . . . . . 8 (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩) = (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩)
7574rnmpt 5910 . . . . . . 7 ran (𝑎 ∈ (V ∩ 𝐴) ↦ ⟨𝑎, 𝑎⟩) = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
7672, 73, 753eqtr3i 2772 . . . . . 6 ran ((𝑎 ∈ V ↦ ⟨𝑎, 𝑎⟩) ↾ 𝐴) = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
7771, 76eqtri 2764 . . . . 5 ran 𝑆 = {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩}
78 elinel2 4156 . . . . . . . . 9 (𝑎 ∈ (V ∩ 𝐴) → 𝑎𝐴)
79 simpl 483 . . . . . . . . . . . 12 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → 𝑎𝐴)
8079, 79opelxpd 5671 . . . . . . . . . . 11 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴))
81 eleq1 2825 . . . . . . . . . . . 12 (𝑝 = ⟨𝑎, 𝑎⟩ → (𝑝 ∈ (𝐴 × 𝐴) ↔ ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴)))
8281adantl 482 . . . . . . . . . . 11 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → (𝑝 ∈ (𝐴 × 𝐴) ↔ ⟨𝑎, 𝑎⟩ ∈ (𝐴 × 𝐴)))
8380, 82mpbird 256 . . . . . . . . . 10 ((𝑎𝐴𝑝 = ⟨𝑎, 𝑎⟩) → 𝑝 ∈ (𝐴 × 𝐴))
8483ex 413 . . . . . . . . 9 (𝑎𝐴 → (𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴)))
8578, 84syl 17 . . . . . . . 8 (𝑎 ∈ (V ∩ 𝐴) → (𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴)))
8685rexlimiv 3145 . . . . . . 7 (∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩ → 𝑝 ∈ (𝐴 × 𝐴))
8786abssi 4027 . . . . . 6 {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩} ⊆ (𝐴 × 𝐴)
8887a1i 11 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → {𝑝 ∣ ∃𝑎 ∈ (V ∩ 𝐴)𝑝 = ⟨𝑎, 𝑎⟩} ⊆ (𝐴 × 𝐴))
8977, 88eqsstrid 3992 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ran 𝑆 ⊆ (𝐴 × 𝐴))
90 fnco 6618 . . . 4 ((𝐻 Fn (𝐴 × 𝐴) ∧ 𝑆 Fn 𝐴 ∧ ran 𝑆 ⊆ (𝐴 × 𝐴)) → (𝐻𝑆) Fn 𝐴)
9165, 70, 89, 90syl3anc 1371 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐻𝑆) Fn 𝐴)
92 opex 5421 . . . . . 6 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V
9392a1i 11 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐴) ∧ 𝑥𝐴) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V)
9493ralrimiva 3143 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → ∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V)
9553fnmpt 6641 . . . 4 (∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
9694, 95syl 17 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
97 eqfnfv 6982 . . 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 1541  wcel 2106  {cab 2713  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  cop 4592  cmpt 5188   I cid 5530   × cxp 5631  ccnv 5632  ran crn 5634  cres 5635  cima 5636  ccom 5637   Fn wfn 6491  cfv 6496  (class class class)co 7357  cmpo 7359  1st c1st 7919  2nd c2nd 7920
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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922
This theorem is referenced by:  offsplitfpar  8051
  Copyright terms: Public domain W3C validator