Metamath Proof Explorer

Theorem tfsconcat0i

Description: The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 28-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2 simpr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
3 fnrel ⊢ ( 𝐴 Fn 𝐶 → Rel 𝐴 )
4 reldm0 ⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )
5 3 4 syl ⊢ ( 𝐴 Fn 𝐶 → ( 𝐴 = ∅ ↔ dom 𝐴 = ∅ ) )
6 fndm ⊢ ( 𝐴 Fn 𝐶 → dom 𝐴 = 𝐶 )
7 6 eqeq1d ⊢ ( 𝐴 Fn 𝐶 → ( dom 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
8 5 7 bitrd ⊢ ( 𝐴 Fn 𝐶 → ( 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
9 8 ad2antrr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ ↔ 𝐶 = ∅ ) )
10 simpr ⊢ ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) → 𝐵 Fn 𝐷 )
11 simpr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → 𝐷 ∈ On )
12 10 11 anim12i ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 Fn 𝐷 ∧ 𝐷 ∈ On ) )
13 12 anim1i ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐶 = ∅ ) → ( ( 𝐵 Fn 𝐷 ∧ 𝐷 ∈ On ) ∧ 𝐶 = ∅ ) )
14 9 13 sylbida ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( ( 𝐵 Fn 𝐷 ∧ 𝐷 ∈ On ) ∧ 𝐶 = ∅ ) )
15 oveq1 ⊢ ( 𝐶 = ∅ → ( 𝐶 +o 𝐷 ) = ( ∅ +o 𝐷 ) )
16 id ⊢ ( 𝐶 = ∅ → 𝐶 = ∅ )
17 15 16 difeq12d ⊢ ( 𝐶 = ∅ → ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) = ( ( ∅ +o 𝐷 ) ∖ ∅ ) )
18 dif0 ⊢ ( ( ∅ +o 𝐷 ) ∖ ∅ ) = ( ∅ +o 𝐷 )
19 17 18 eqtrdi ⊢ ( 𝐶 = ∅ → ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) = ( ∅ +o 𝐷 ) )
20 19 eleq2d ⊢ ( 𝐶 = ∅ → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ 𝑥 ∈ ( ∅ +o 𝐷 ) ) )
21 oveq1 ⊢ ( 𝐶 = ∅ → ( 𝐶 +o 𝑧 ) = ( ∅ +o 𝑧 ) )
22 21 eqeq2d ⊢ ( 𝐶 = ∅ → ( 𝑥 = ( 𝐶 +o 𝑧 ) ↔ 𝑥 = ( ∅ +o 𝑧 ) ) )
23 22 anbi1d ⊢ ( 𝐶 = ∅ → ( ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
24 23 rexbidv ⊢ ( 𝐶 = ∅ → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
25 20 24 anbi12d ⊢ ( 𝐶 = ∅ → ( ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝑥 ∈ ( ∅ +o 𝐷 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ) )
26 oa0r ⊢ ( 𝐷 ∈ On → ( ∅ +o 𝐷 ) = 𝐷 )
27 26 eleq2d ⊢ ( 𝐷 ∈ On → ( 𝑥 ∈ ( ∅ +o 𝐷 ) ↔ 𝑥 ∈ 𝐷 ) )
28 onelon ⊢ ( ( 𝐷 ∈ On ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ On )
29 oa0r ⊢ ( 𝑧 ∈ On → ( ∅ +o 𝑧 ) = 𝑧 )
30 29 eqeq2d ⊢ ( 𝑧 ∈ On → ( 𝑥 = ( ∅ +o 𝑧 ) ↔ 𝑥 = 𝑧 ) )
31 30 anbi1d ⊢ ( 𝑧 ∈ On → ( ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
32 28 31 syl ⊢ ( ( 𝐷 ∈ On ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
33 32 rexbidva ⊢ ( 𝐷 ∈ On → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
34 27 33 anbi12d ⊢ ( 𝐷 ∈ On → ( ( 𝑥 ∈ ( ∅ +o 𝐷 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ) )
35 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
36 an12 ⊢ ( ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝑥 = 𝑧 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
37 eqcom ⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
38 37 anbi1i ⊢ ( ( 𝑥 = 𝑧 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
39 36 38 bitri ⊢ ( ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
40 39 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐷 ∧ ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
41 eleq1w ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝐷 ↔ 𝑥 ∈ 𝐷 ) )
42 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐵 ‘ 𝑧 ) = ( 𝐵 ‘ 𝑥 ) )
43 42 eqeq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑦 = ( 𝐵 ‘ 𝑧 ) ↔ 𝑦 = ( 𝐵 ‘ 𝑥 ) ) )
44 41 43 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑥 ) ) ) )
45 44 equsexvw ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑥 ) ) )
46 35 40 45 3bitri ⊢ ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑦 = ( 𝐵 ‘ 𝑥 ) ) )
47 46 baib ⊢ ( 𝑥 ∈ 𝐷 → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ 𝑦 = ( 𝐵 ‘ 𝑥 ) ) )
48 47 adantl ⊢ ( ( 𝐵 Fn 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ 𝑦 = ( 𝐵 ‘ 𝑥 ) ) )
49 eqcom ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑥 ) ↔ ( 𝐵 ‘ 𝑥 ) = 𝑦 )
50 48 49 bitrdi ⊢ ( ( 𝐵 Fn 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝐵 ‘ 𝑥 ) = 𝑦 ) )
51 fnbrfvb ⊢ ( ( 𝐵 Fn 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐵 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
52 50 51 bitrd ⊢ ( ( 𝐵 Fn 𝐷 ∧ 𝑥 ∈ 𝐷 ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ 𝑥 𝐵 𝑦 ) )
53 52 pm5.32da ⊢ ( 𝐵 Fn 𝐷 → ( ( 𝑥 ∈ 𝐷 ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑥 𝐵 𝑦 ) ) )
54 fnbr ⊢ ( ( 𝐵 Fn 𝐷 ∧ 𝑥 𝐵 𝑦 ) → 𝑥 ∈ 𝐷 )
55 54 ex ⊢ ( 𝐵 Fn 𝐷 → ( 𝑥 𝐵 𝑦 → 𝑥 ∈ 𝐷 ) )
56 55 pm4.71rd ⊢ ( 𝐵 Fn 𝐷 → ( 𝑥 𝐵 𝑦 ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑥 𝐵 𝑦 ) ) )
57 df-br ⊢ ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
58 56 57 bitr3di ⊢ ( 𝐵 Fn 𝐷 → ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 𝐵 𝑦 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
59 53 58 bitrd ⊢ ( 𝐵 Fn 𝐷 → ( ( 𝑥 ∈ 𝐷 ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = 𝑧 ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
60 34 59 sylan9bbr ⊢ ( ( 𝐵 Fn 𝐷 ∧ 𝐷 ∈ On ) → ( ( 𝑥 ∈ ( ∅ +o 𝐷 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( ∅ +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
61 25 60 sylan9bbr ⊢ ( ( ( 𝐵 Fn 𝐷 ∧ 𝐷 ∈ On ) ∧ 𝐶 = ∅ ) → ( ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
62 61 opabbidv ⊢ ( ( ( 𝐵 Fn 𝐷 ∧ 𝐷 ∈ On ) ∧ 𝐶 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } )
63 14 62 syl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } )
64 fnrel ⊢ ( 𝐵 Fn 𝐷 → Rel 𝐵 )
65 opabid2 ⊢ ( Rel 𝐵 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
66 64 65 syl ⊢ ( 𝐵 Fn 𝐷 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
67 66 adantl ⊢ ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
68 67 ad2antrr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 } = 𝐵 )
69 63 68 eqtrd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = 𝐵 )
70 2 69 uneq12d ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = ( ∅ ∪ 𝐵 ) )
71 0un ⊢ ( ∅ ∪ 𝐵 ) = 𝐵
72 70 71 eqtrdi ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = 𝐵 )
73 72 ex ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ → ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = 𝐵 ) )
74 1 tfsconcatun ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) = ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
75 74 eqeq1d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 + 𝐵 ) = 𝐵 ↔ ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = 𝐵 ) )
76 73 75 sylibrd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ → ( 𝐴 + 𝐵 ) = 𝐵 ) )