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