Metamath Proof Explorer

Theorem tfsconcatfv

Description: The value of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2 1 tfsconcatfv1 ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 + 𝐵 ) ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) )
3 2 adantlr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 + 𝐵 ) ‘ 𝑋 ) = ( 𝐴 ‘ 𝑋 ) )
4 simpr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ 𝐶 )
5 4 iftrued ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ 𝑋 ∈ 𝐶 ) → if ( 𝑋 ∈ 𝐶 , ( 𝐴 ‘ 𝑋 ) , ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) = ( 𝐴 ‘ 𝑋 ) )
6 3 5 eqtr4d ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 + 𝐵 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐶 , ( 𝐴 ‘ 𝑋 ) , ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) )
7 simpr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ¬ 𝑋 ∈ 𝐶 )
8 7 iffalsed ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → if ( 𝑋 ∈ 𝐶 , ( 𝐴 ‘ 𝑋 ) , ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) = ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) )
9 simpll ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) )
10 onss ⊢ ( 𝐷 ∈ On → 𝐷 ⊆ On )
11 10 adantl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → 𝐷 ⊆ On )
12 11 ad3antlr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → 𝐷 ⊆ On )
13 simpllr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) )
14 simplrl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) → 𝐶 ∈ On )
15 oacl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 +o 𝐷 ) ∈ On )
16 15 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐶 +o 𝐷 ) ∈ On )
17 onelon ⊢ ( ( ( 𝐶 +o 𝐷 ) ∈ On ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) → 𝑋 ∈ On )
18 16 17 sylan ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) → 𝑋 ∈ On )
19 ontri1 ⊢ ( ( 𝐶 ∈ On ∧ 𝑋 ∈ On ) → ( 𝐶 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝐶 ) )
20 14 18 19 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) → ( 𝐶 ⊆ 𝑋 ↔ ¬ 𝑋 ∈ 𝐶 ) )
21 20 biimpar ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → 𝐶 ⊆ 𝑋 )
22 simplr ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( 𝐶 +o 𝐷 ) )
23 oawordex2 ⊢ ( ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ∧ ( 𝐶 ⊆ 𝑋 ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ) → ∃ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 )
24 13 21 22 23 syl12anc ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ∃ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 )
25 14 18 jca ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) → ( 𝐶 ∈ On ∧ 𝑋 ∈ On ) )
26 oawordeu ⊢ ( ( ( 𝐶 ∈ On ∧ 𝑋 ∈ On ) ∧ 𝐶 ⊆ 𝑋 ) → ∃! 𝑑 ∈ On ( 𝐶 +o 𝑑 ) = 𝑋 )
27 25 21 26 syl2an2r ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ∃! 𝑑 ∈ On ( 𝐶 +o 𝑑 ) = 𝑋 )
28 reuss ⊢ ( ( 𝐷 ⊆ On ∧ ∃ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ∧ ∃! 𝑑 ∈ On ( 𝐶 +o 𝑑 ) = 𝑋 ) → ∃! 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 )
29 12 24 27 28 syl3anc ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ∃! 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 )
30 riotacl ⊢ ( ∃! 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 → ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 )
31 29 30 syl ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 )
32 1 tfsconcatfv2 ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 ) → ( ( 𝐴 + 𝐵 ) ‘ ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) = ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) )
33 9 31 32 syl2anc ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 + 𝐵 ) ‘ ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) = ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) )
34 riotasbc ⊢ ( ∃! 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 → [ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ] ( 𝐶 +o 𝑑 ) = 𝑋 )
35 29 34 syl ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → [ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ] ( 𝐶 +o 𝑑 ) = 𝑋 )
36 sbceq1g ⊢ ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 → ( [ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ] ( 𝐶 +o 𝑑 ) = 𝑋 ↔ ⦋ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ⦌ ( 𝐶 +o 𝑑 ) = 𝑋 ) )
37 csbov2g ⊢ ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 → ⦋ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ⦌ ( 𝐶 +o 𝑑 ) = ( 𝐶 +o ⦋ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ⦌ 𝑑 ) )
38 csbvarg ⊢ ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 → ⦋ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ⦌ 𝑑 = ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) )
39 38 oveq2d ⊢ ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 → ( 𝐶 +o ⦋ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ⦌ 𝑑 ) = ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) )
40 37 39 eqtrd ⊢ ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 → ⦋ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ⦌ ( 𝐶 +o 𝑑 ) = ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) )
41 40 eqeq1d ⊢ ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 → ( ⦋ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ⦌ ( 𝐶 +o 𝑑 ) = 𝑋 ↔ ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) = 𝑋 ) )
42 36 41 bitrd ⊢ ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 → ( [ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ] ( 𝐶 +o 𝑑 ) = 𝑋 ↔ ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) = 𝑋 ) )
43 42 biimpa ⊢ ( ( ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ∈ 𝐷 ∧ [ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) / 𝑑 ] ( 𝐶 +o 𝑑 ) = 𝑋 ) → ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) = 𝑋 )
44 31 35 43 syl2anc ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) = 𝑋 )
45 44 fveq2d ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 + 𝐵 ) ‘ ( 𝐶 +o ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) = ( ( 𝐴 + 𝐵 ) ‘ 𝑋 ) )
46 8 33 45 3eqtr2rd ⊢ ( ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) ∧ ¬ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 + 𝐵 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐶 , ( 𝐴 ‘ 𝑋 ) , ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) )
47 6 46 pm2.61dan ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝑋 ∈ ( 𝐶 +o 𝐷 ) ) → ( ( 𝐴 + 𝐵 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐶 , ( 𝐴 ‘ 𝑋 ) , ( 𝐵 ‘ ( ℩ 𝑑 ∈ 𝐷 ( 𝐶 +o 𝑑 ) = 𝑋 ) ) ) )