Theorem tfsconcat00

Description: The concatentation of two empty series results in an empty series. (Contributed by RP, 25-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		tfsconcat.op	⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2	1	tfsconcatrn	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ran ( 𝐴 + 𝐵 ) = ( ran 𝐴 ∪ ran 𝐵 ) )
3	2	eqeq1d	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ran ( 𝐴 + 𝐵 ) = ∅ ↔ ( ran 𝐴 ∪ ran 𝐵 ) = ∅ ) )
4	1	tfsconcatfn	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) Fn ( 𝐶 +o 𝐷 ) )
5		fnrel	⊢ ( ( 𝐴 + 𝐵 ) Fn ( 𝐶 +o 𝐷 ) → Rel ( 𝐴 + 𝐵 ) )
6		relrn0	⊢ ( Rel ( 𝐴 + 𝐵 ) → ( ( 𝐴 + 𝐵 ) = ∅ ↔ ran ( 𝐴 + 𝐵 ) = ∅ ) )
7	4 5 6	3syl	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 + 𝐵 ) = ∅ ↔ ran ( 𝐴 + 𝐵 ) = ∅ ) )
8		fnrel	⊢ ( 𝐴 Fn 𝐶 → Rel 𝐴 )
9		relrn0	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ran 𝐴 = ∅ ) )
10	8 9	syl	⊢ ( 𝐴 Fn 𝐶 → ( 𝐴 = ∅ ↔ ran 𝐴 = ∅ ) )
11		fnrel	⊢ ( 𝐵 Fn 𝐷 → Rel 𝐵 )
12		relrn0	⊢ ( Rel 𝐵 → ( 𝐵 = ∅ ↔ ran 𝐵 = ∅ ) )
13	11 12	syl	⊢ ( 𝐵 Fn 𝐷 → ( 𝐵 = ∅ ↔ ran 𝐵 = ∅ ) )
14	10 13	bi2anan9	⊢ ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) → ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( ran 𝐴 = ∅ ∧ ran 𝐵 = ∅ ) ) )
15		un00	⊢ ( ( ran 𝐴 = ∅ ∧ ran 𝐵 = ∅ ) ↔ ( ran 𝐴 ∪ ran 𝐵 ) = ∅ )
16	14 15	bitrdi	⊢ ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) → ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( ran 𝐴 ∪ ran 𝐵 ) = ∅ ) )
17	16	adantr	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( ran 𝐴 ∪ ran 𝐵 ) = ∅ ) )
18	3 7 17	3bitr4rd	⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ↔ ( 𝐴 + 𝐵 ) = ∅ ) )