Metamath Proof Explorer

Theorem tfsconcatfv2

Description: A latter value of the concatenation of two transfinite series. (Contributed by RP, 23-Feb-2025)

Ref Expression
Hypothesis tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
Assertion tfsconcatfv2 ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐴 + 𝐵 ) ‘ ( 𝐶 +o 𝑋 ) ) = ( 𝐵 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2 1 tfsconcatun ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) = ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
3 2 fveq1d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 + 𝐵 ) ‘ ( 𝐶 +o 𝑋 ) ) = ( ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) ‘ ( 𝐶 +o 𝑋 ) ) )
4 3 adantr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐴 + 𝐵 ) ‘ ( 𝐶 +o 𝑋 ) ) = ( ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) ‘ ( 𝐶 +o 𝑋 ) ) )
5 simplll ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → 𝐴 Fn 𝐶 )
6 simplrl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → 𝐶 ∈ On )
7 simplrr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → 𝐷 ∈ On )
8 simpr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) )
9 tfsconcatlem ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ∃! 𝑦 ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ∃! 𝑦 ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) )
11 10 ralrimiva ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ∀ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∃! 𝑦 ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) )
12 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) }
13 12 fnopabg ⊢ ( ∀ 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∃! 𝑦 ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } Fn ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) )
14 11 13 sylib ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } Fn ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) )
15 14 adantr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } Fn ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) )
16 disjdif ⊢ ( 𝐶 ∩ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) = ∅
17 16 a1i ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( 𝐶 ∩ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) = ∅ )
18 pm3.22 ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) )
19 18 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) )
20 oaordi ⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑋 ∈ 𝐷 → ( 𝐶 +o 𝑋 ) ∈ ( 𝐶 +o 𝐷 ) ) )
21 19 20 syl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝑋 ∈ 𝐷 → ( 𝐶 +o 𝑋 ) ∈ ( 𝐶 +o 𝐷 ) ) )
22 21 imp ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( 𝐶 +o 𝑋 ) ∈ ( 𝐶 +o 𝐷 ) )
23 simplrl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → 𝐶 ∈ On )
24 simpr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → 𝐷 ∈ On )
25 24 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐷 ∈ On )
26 onelon ⊢ ( ( 𝐷 ∈ On ∧ 𝑋 ∈ 𝐷 ) → 𝑋 ∈ On )
27 25 26 sylan ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → 𝑋 ∈ On )
28 oaword1 ⊢ ( ( 𝐶 ∈ On ∧ 𝑋 ∈ On ) → 𝐶 ⊆ ( 𝐶 +o 𝑋 ) )
29 23 27 28 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → 𝐶 ⊆ ( 𝐶 +o 𝑋 ) )
30 oacl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 +o 𝐷 ) ∈ On )
31 eloni ⊢ ( ( 𝐶 +o 𝐷 ) ∈ On → Ord ( 𝐶 +o 𝐷 ) )
32 30 31 syl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord ( 𝐶 +o 𝐷 ) )
33 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
34 33 adantr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord 𝐶 )
35 32 34 jca ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) )
36 35 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) )
37 36 adantr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) )
38 ordeldif ⊢ ( ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) → ( ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( ( 𝐶 +o 𝑋 ) ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ ( 𝐶 +o 𝑋 ) ) ) )
39 37 38 syl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( ( 𝐶 +o 𝑋 ) ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ ( 𝐶 +o 𝑋 ) ) ) )
40 22 29 39 mpbir2and ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) )
41 5 15 17 40 fvun2d ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) ‘ ( 𝐶 +o 𝑋 ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ‘ ( 𝐶 +o 𝑋 ) ) )
42 eqid ⊢ ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑋 )
43 eqid ⊢ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 )
44 oveq2 ⊢ ( 𝑧 = 𝑋 → ( 𝐶 +o 𝑧 ) = ( 𝐶 +o 𝑋 ) )
45 44 eqeq2d ⊢ ( 𝑧 = 𝑋 → ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ↔ ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑋 ) ) )
46 fveq2 ⊢ ( 𝑧 = 𝑋 → ( 𝐵 ‘ 𝑧 ) = ( 𝐵 ‘ 𝑋 ) )
47 46 eqeq2d ⊢ ( 𝑧 = 𝑋 → ( ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ↔ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) )
48 45 47 anbi12d ⊢ ( 𝑧 = 𝑋 → ( ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) ↔ ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑋 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) ) )
49 48 rspcev ⊢ ( ( 𝑋 ∈ 𝐷 ∧ ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑋 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑋 ) ) ) → ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) )
50 42 43 49 mpanr12 ⊢ ( 𝑋 ∈ 𝐷 → ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) )
51 50 adantl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) )
52 ovex ⊢ ( 𝐶 +o 𝑋 ) ∈ V
53 fvex ⊢ ( 𝐵 ‘ 𝑋 ) ∈ V
54 52 53 pm3.2i ⊢ ( ( 𝐶 +o 𝑋 ) ∈ V ∧ ( 𝐵 ‘ 𝑋 ) ∈ V )
55 eleq1 ⊢ ( 𝑥 = ( 𝐶 +o 𝑋 ) → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) )
56 eqeq1 ⊢ ( 𝑥 = ( 𝐶 +o 𝑋 ) → ( 𝑥 = ( 𝐶 +o 𝑧 ) ↔ ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ) )
57 56 anbi1d ⊢ ( 𝑥 = ( 𝐶 +o 𝑋 ) → ( ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
58 57 rexbidv ⊢ ( 𝑥 = ( 𝐶 +o 𝑋 ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
59 55 58 anbi12d ⊢ ( 𝑥 = ( 𝐶 +o 𝑋 ) → ( ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ) )
60 eqeq1 ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑋 ) → ( 𝑦 = ( 𝐵 ‘ 𝑧 ) ↔ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) )
61 60 anbi2d ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑋 ) → ( ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) ) )
62 61 rexbidv ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑋 ) → ( ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) ) )
63 62 anbi2d ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑋 ) → ( ( ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) ) ) )
64 59 63 opelopabg ⊢ ( ( ( 𝐶 +o 𝑋 ) ∈ V ∧ ( 𝐵 ‘ 𝑋 ) ∈ V ) → ( ⟨ ( 𝐶 +o 𝑋 ) , ( 𝐵 ‘ 𝑋 ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ↔ ( ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) ) ) )
65 54 64 mp1i ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( ⟨ ( 𝐶 +o 𝑋 ) , ( 𝐵 ‘ 𝑋 ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ↔ ( ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( ( 𝐶 +o 𝑋 ) = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ 𝑋 ) = ( 𝐵 ‘ 𝑧 ) ) ) ) )
66 40 51 65 mpbir2and ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ⟨ ( 𝐶 +o 𝑋 ) , ( 𝐵 ‘ 𝑋 ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } )
67 fnopfvb ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } Fn ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ( 𝐶 +o 𝑋 ) ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) → ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ‘ ( 𝐶 +o 𝑋 ) ) = ( 𝐵 ‘ 𝑋 ) ↔ ⟨ ( 𝐶 +o 𝑋 ) , ( 𝐵 ‘ 𝑋 ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
68 15 40 67 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ‘ ( 𝐶 +o 𝑋 ) ) = ( 𝐵 ‘ 𝑋 ) ↔ ⟨ ( 𝐶 +o 𝑋 ) , ( 𝐵 ‘ 𝑋 ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
69 66 68 mpbird ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ‘ ( 𝐶 +o 𝑋 ) ) = ( 𝐵 ‘ 𝑋 ) )
70 4 41 69 3eqtrd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐴 + 𝐵 ) ‘ ( 𝐶 +o 𝑋 ) ) = ( 𝐵 ‘ 𝑋 ) )