Metamath Proof Explorer

Theorem tfsconcatrev

Description: If the domain of a transfinite sequence is an ordinal sum, the sequence can be decomposed into two sequences with domains corresponding to the addends. Theorem 2 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025)

Ref Expression
Hypothesis tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
Assertion tfsconcatrev ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ∃ 𝑢 ∈ ( ran 𝐹 ↑m 𝐶 ) ∃ 𝑣 ∈ ( ran 𝐹 ↑m 𝐷 ) ( ( 𝑢 + 𝑣 ) = 𝐹 ∧ dom 𝑢 = 𝐶 ∧ dom 𝑣 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2 dffn3 ⊢ ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ↔ 𝐹 : ( 𝐶 +o 𝐷 ) ⟶ ran 𝐹 )
3 2 birani ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐹 : ( 𝐶 +o 𝐷 ) ⟶ ran 𝐹 )
4 fndm ⊢ ( 𝐹 Fn ( 𝐶 +o 𝐷 ) → dom 𝐹 = ( 𝐶 +o 𝐷 ) )
5 4 adantr ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → dom 𝐹 = ( 𝐶 +o 𝐷 ) )
6 oacl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 +o 𝐷 ) ∈ On )
7 6 adantl ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 +o 𝐷 ) ∈ On )
8 5 7 eqeltrd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → dom 𝐹 ∈ On )
9 fnfun ⊢ ( 𝐹 Fn ( 𝐶 +o 𝐷 ) → Fun 𝐹 )
10 9 adantr ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → Fun 𝐹 )
11 funrnex ⊢ ( dom 𝐹 ∈ On → ( Fun 𝐹 → ran 𝐹 ∈ V ) )
12 8 10 11 sylc ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran 𝐹 ∈ V )
13 12 7 elmapd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐹 ∈ ( ran 𝐹 ↑m ( 𝐶 +o 𝐷 ) ) ↔ 𝐹 : ( 𝐶 +o 𝐷 ) ⟶ ran 𝐹 ) )
14 3 13 mpbird ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐹 ∈ ( ran 𝐹 ↑m ( 𝐶 +o 𝐷 ) ) )
15 oaword1 ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → 𝐶 ⊆ ( 𝐶 +o 𝐷 ) )
16 15 adantl ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐶 ⊆ ( 𝐶 +o 𝐷 ) )
17 elmapssres ⊢ ( ( 𝐹 ∈ ( ran 𝐹 ↑m ( 𝐶 +o 𝐷 ) ) ∧ 𝐶 ⊆ ( 𝐶 +o 𝐷 ) ) → ( 𝐹 ↾ 𝐶 ) ∈ ( ran 𝐹 ↑m 𝐶 ) )
18 14 16 17 syl2anc ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐹 ↾ 𝐶 ) ∈ ( ran 𝐹 ↑m 𝐶 ) )
19 simpl ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐹 Fn ( 𝐶 +o 𝐷 ) )
20 oaordi ⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑑 ∈ 𝐷 → ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ) )
21 20 ancoms ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝑑 ∈ 𝐷 → ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ) )
22 21 adantl ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑑 ∈ 𝐷 → ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ) )
23 22 imp ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) )
24 fnfvelrn ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 +o 𝑑 ) ∈ ( 𝐶 +o 𝐷 ) ) → ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ∈ ran 𝐹 )
25 19 23 24 syl2an2r ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ∈ ran 𝐹 )
26 25 fmpttd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) : 𝐷 ⟶ ran 𝐹 )
27 simprr ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐷 ∈ On )
28 12 27 elmapd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ∈ ( ran 𝐹 ↑m 𝐷 ) ↔ ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) : 𝐷 ⟶ ran 𝐹 ) )
29 26 28 mpbird ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ∈ ( ran 𝐹 ↑m 𝐷 ) )
30 19 16 fnssresd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐹 ↾ 𝐶 ) Fn 𝐶 )
31 fvex ⊢ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ∈ V
32 eqid ⊢ ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) = ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) )
33 31 32 fnmpti ⊢ ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) Fn 𝐷
34 33 a1i ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) Fn 𝐷 )
35 simpr ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) )
36 1 tfsconcatun ⊢ ( ( ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) = ( ( 𝐹 ↾ 𝐶 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) } ) )
37 30 34 35 36 syl21anc ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) = ( ( 𝐹 ↾ 𝐶 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) } ) )
38 oveq2 ⊢ ( 𝑑 = 𝑧 → ( 𝐶 +o 𝑑 ) = ( 𝐶 +o 𝑧 ) )
39 38 fveq2d ⊢ ( 𝑑 = 𝑧 → ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) = ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) )
40 fvex ⊢ ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) ∈ V
41 39 32 40 fvmpt ⊢ ( 𝑧 ∈ 𝐷 → ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) )
42 41 ad2antlr ⊢ ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) )
43 fveq2 ⊢ ( 𝑥 = ( 𝐶 +o 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) )
44 43 adantl ⊢ ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) )
45 42 44 eqtr4d ⊢ ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
46 45 eqeq2d ⊢ ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
47 46 biimpd ⊢ ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑥 = ( 𝐶 +o 𝑧 ) ) → ( 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
48 47 expimpd ⊢ ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
49 48 rexlimdva ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
50 simplr ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) )
51 eloni ⊢ ( ( 𝐶 +o 𝐷 ) ∈ On → Ord ( 𝐶 +o 𝐷 ) )
52 6 51 syl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord ( 𝐶 +o 𝐷 ) )
53 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
54 53 adantr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord 𝐶 )
55 ordeldif ⊢ ( ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝑥 ) ) )
56 52 54 55 syl2anc ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝑥 ) ) )
57 56 adantl ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝑥 ) ) )
58 57 biimpa ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝑥 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝑥 ) )
59 58 ancomd ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝐶 ⊆ 𝑥 ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) )
60 50 59 jca ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐶 ⊆ 𝑥 ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) ) )
61 60 adantr ⊢ ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐶 ⊆ 𝑥 ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) ) )
62 oawordex2 ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐶 ⊆ 𝑥 ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) ) → ∃ 𝑧 ∈ 𝐷 ( 𝐶 +o 𝑧 ) = 𝑥 )
63 61 62 syl ⊢ ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐷 ( 𝐶 +o 𝑧 ) = 𝑥 )
64 simpr ⊢ ( ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 +o 𝑧 ) = 𝑥 ) → ( 𝐶 +o 𝑧 ) = 𝑥 )
65 64 eqcomd ⊢ ( ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 +o 𝑧 ) = 𝑥 ) → 𝑥 = ( 𝐶 +o 𝑧 ) )
66 64 fveq2d ⊢ ( ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 +o 𝑧 ) = 𝑥 ) → ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) = ( 𝐹 ‘ 𝑥 ) )
67 41 ad2antlr ⊢ ( ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 +o 𝑧 ) = 𝑥 ) → ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐶 +o 𝑧 ) ) )
68 simpllr ⊢ ( ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 +o 𝑧 ) = 𝑥 ) → 𝑦 = ( 𝐹 ‘ 𝑥 ) )
69 66 67 68 3eqtr4rd ⊢ ( ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 +o 𝑧 ) = 𝑥 ) → 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) )
70 65 69 jca ⊢ ( ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 +o 𝑧 ) = 𝑥 ) → ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) )
71 70 ex ⊢ ( ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝐶 +o 𝑧 ) = 𝑥 → ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) )
72 71 reximdva ⊢ ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝐶 +o 𝑧 ) = 𝑥 → ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) )
73 63 72 mpd ⊢ ( ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) )
74 73 ex ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) )
75 49 74 impbid ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) )
76 eldifi ⊢ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) → 𝑥 ∈ ( 𝐶 +o 𝐷 ) )
77 eqcom ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 )
78 fnbrfvb ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
79 77 78 bitrid ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ 𝑥 ∈ ( 𝐶 +o 𝐷 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
80 19 76 79 syl2an ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
81 75 80 bitrd ⊢ ( ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ↔ 𝑥 𝐹 𝑦 ) )
82 81 pm5.32da ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) ↔ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ 𝑥 𝐹 𝑦 ) ) )
83 82 opabbidv ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ 𝑥 𝐹 𝑦 ) } )
84 dfres2 ⊢ ( 𝐹 ↾ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ 𝑥 𝐹 𝑦 ) }
85 83 84 eqtr4di ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) } = ( 𝐹 ↾ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) )
86 85 uneq2d ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐹 ↾ 𝐶 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ‘ 𝑧 ) ) ) } ) = ( ( 𝐹 ↾ 𝐶 ) ∪ ( 𝐹 ↾ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ) )
87 37 86 eqtrd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) = ( ( 𝐹 ↾ 𝐶 ) ∪ ( 𝐹 ↾ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ) )
88 resundi ⊢ ( 𝐹 ↾ ( 𝐶 ∪ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ) = ( ( 𝐹 ↾ 𝐶 ) ∪ ( 𝐹 ↾ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) )
89 88 a1i ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐹 ↾ ( 𝐶 ∪ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ) = ( ( 𝐹 ↾ 𝐶 ) ∪ ( 𝐹 ↾ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ) )
90 undif ⊢ ( 𝐶 ⊆ ( 𝐶 +o 𝐷 ) ↔ ( 𝐶 ∪ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) = ( 𝐶 +o 𝐷 ) )
91 15 90 sylib ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 ∪ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) = ( 𝐶 +o 𝐷 ) )
92 91 adantl ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∪ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) = ( 𝐶 +o 𝐷 ) )
93 92 reseq2d ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐹 ↾ ( 𝐶 ∪ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ) = ( 𝐹 ↾ ( 𝐶 +o 𝐷 ) ) )
94 fnresdm ⊢ ( 𝐹 Fn ( 𝐶 +o 𝐷 ) → ( 𝐹 ↾ ( 𝐶 +o 𝐷 ) ) = 𝐹 )
95 94 adantr ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐹 ↾ ( 𝐶 +o 𝐷 ) ) = 𝐹 )
96 93 95 eqtrd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐹 ↾ ( 𝐶 ∪ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) ) = 𝐹 )
97 87 89 96 3eqtr2d ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) = 𝐹 )
98 dmres ⊢ dom ( 𝐹 ↾ 𝐶 ) = ( 𝐶 ∩ dom 𝐹 )
99 16 5 sseqtrrd ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐶 ⊆ dom 𝐹 )
100 dfss2 ⊢ ( 𝐶 ⊆ dom 𝐹 ↔ ( 𝐶 ∩ dom 𝐹 ) = 𝐶 )
101 99 100 sylib ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∩ dom 𝐹 ) = 𝐶 )
102 98 101 eqtrid ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → dom ( 𝐹 ↾ 𝐶 ) = 𝐶 )
103 31 32 dmmpti ⊢ dom ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) = 𝐷
104 103 a1i ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → dom ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) = 𝐷 )
105 oveq1 ⊢ ( 𝑢 = ( 𝐹 ↾ 𝐶 ) → ( 𝑢 + 𝑣 ) = ( ( 𝐹 ↾ 𝐶 ) + 𝑣 ) )
106 105 eqeq1d ⊢ ( 𝑢 = ( 𝐹 ↾ 𝐶 ) → ( ( 𝑢 + 𝑣 ) = 𝐹 ↔ ( ( 𝐹 ↾ 𝐶 ) + 𝑣 ) = 𝐹 ) )
107 dmeq ⊢ ( 𝑢 = ( 𝐹 ↾ 𝐶 ) → dom 𝑢 = dom ( 𝐹 ↾ 𝐶 ) )
108 107 eqeq1d ⊢ ( 𝑢 = ( 𝐹 ↾ 𝐶 ) → ( dom 𝑢 = 𝐶 ↔ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ) )
109 106 108 3anbi12d ⊢ ( 𝑢 = ( 𝐹 ↾ 𝐶 ) → ( ( ( 𝑢 + 𝑣 ) = 𝐹 ∧ dom 𝑢 = 𝐶 ∧ dom 𝑣 = 𝐷 ) ↔ ( ( ( 𝐹 ↾ 𝐶 ) + 𝑣 ) = 𝐹 ∧ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ∧ dom 𝑣 = 𝐷 ) ) )
110 oveq2 ⊢ ( 𝑣 = ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) → ( ( 𝐹 ↾ 𝐶 ) + 𝑣 ) = ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) )
111 110 eqeq1d ⊢ ( 𝑣 = ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) → ( ( ( 𝐹 ↾ 𝐶 ) + 𝑣 ) = 𝐹 ↔ ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) = 𝐹 ) )
112 dmeq ⊢ ( 𝑣 = ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) → dom 𝑣 = dom ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) )
113 112 eqeq1d ⊢ ( 𝑣 = ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) → ( dom 𝑣 = 𝐷 ↔ dom ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) = 𝐷 ) )
114 111 113 3anbi13d ⊢ ( 𝑣 = ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) → ( ( ( ( 𝐹 ↾ 𝐶 ) + 𝑣 ) = 𝐹 ∧ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ∧ dom 𝑣 = 𝐷 ) ↔ ( ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) = 𝐹 ∧ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ∧ dom ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) = 𝐷 ) ) )
115 109 114 rspc2ev ⊢ ( ( ( 𝐹 ↾ 𝐶 ) ∈ ( ran 𝐹 ↑m 𝐶 ) ∧ ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ∈ ( ran 𝐹 ↑m 𝐷 ) ∧ ( ( ( 𝐹 ↾ 𝐶 ) + ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) ) = 𝐹 ∧ dom ( 𝐹 ↾ 𝐶 ) = 𝐶 ∧ dom ( 𝑑 ∈ 𝐷 ↦ ( 𝐹 ‘ ( 𝐶 +o 𝑑 ) ) ) = 𝐷 ) ) → ∃ 𝑢 ∈ ( ran 𝐹 ↑m 𝐶 ) ∃ 𝑣 ∈ ( ran 𝐹 ↑m 𝐷 ) ( ( 𝑢 + 𝑣 ) = 𝐹 ∧ dom 𝑢 = 𝐶 ∧ dom 𝑣 = 𝐷 ) )
116 18 29 97 102 104 115 syl113anc ⊢ ( ( 𝐹 Fn ( 𝐶 +o 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ∃ 𝑢 ∈ ( ran 𝐹 ↑m 𝐶 ) ∃ 𝑣 ∈ ( ran 𝐹 ↑m 𝐷 ) ( ( 𝑢 + 𝑣 ) = 𝐹 ∧ dom 𝑢 = 𝐶 ∧ dom 𝑣 = 𝐷 ) )