Metamath Proof Explorer

Theorem tfsconcatb0

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

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

Proof

Step Hyp Ref Expression
1 tfsconcat.op ⊢ + = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑎 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( dom 𝑎 +o dom 𝑏 ) ∖ dom 𝑎 ) ∧ ∃ 𝑧 ∈ dom 𝑏 ( 𝑥 = ( dom 𝑎 +o 𝑧 ) ∧ 𝑦 = ( 𝑏 ‘ 𝑧 ) ) ) } ) )
2 fnrel ⊢ ( 𝐵 Fn 𝐷 → Rel 𝐵 )
3 reldm0 ⊢ ( Rel 𝐵 → ( 𝐵 = ∅ ↔ dom 𝐵 = ∅ ) )
4 2 3 syl ⊢ ( 𝐵 Fn 𝐷 → ( 𝐵 = ∅ ↔ dom 𝐵 = ∅ ) )
5 fndm ⊢ ( 𝐵 Fn 𝐷 → dom 𝐵 = 𝐷 )
6 5 eqeq1d ⊢ ( 𝐵 Fn 𝐷 → ( dom 𝐵 = ∅ ↔ 𝐷 = ∅ ) )
7 4 6 bitrd ⊢ ( 𝐵 Fn 𝐷 → ( 𝐵 = ∅ ↔ 𝐷 = ∅ ) )
8 7 ad2antlr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 = ∅ ↔ 𝐷 = ∅ ) )
9 rex0 ⊢ ¬ ∃ 𝑧 ∈ ∅ ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) )
10 rexeq ⊢ ( 𝐷 = ∅ → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ ∅ ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
11 10 adantl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐷 = ∅ ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ ∅ ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
12 9 11 mtbiri ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐷 = ∅ ) → ¬ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) )
13 12 intnand ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐷 = ∅ ) → ¬ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
14 13 alrimivv ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐷 = ∅ ) → ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
15 opab0 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) )
16 14 15 sylibr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐷 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } = ∅ )
17 0ss ⊢ ∅ ⊆ 𝐴
18 16 17 eqsstrdi ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 𝐷 = ∅ ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 )
19 18 ex ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐷 = ∅ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 ) )
20 df-1o ⊢ 1o = suc ∅
21 simpl ⊢ ( ( 𝐷 ∈ On ∧ ¬ 𝐷 = ∅ ) → 𝐷 ∈ On )
22 on0eln0 ⊢ ( 𝐷 ∈ On → ( ∅ ∈ 𝐷 ↔ 𝐷 ≠ ∅ ) )
23 df-ne ⊢ ( 𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅ )
24 22 23 bitrdi ⊢ ( 𝐷 ∈ On → ( ∅ ∈ 𝐷 ↔ ¬ 𝐷 = ∅ ) )
25 24 biimpar ⊢ ( ( 𝐷 ∈ On ∧ ¬ 𝐷 = ∅ ) → ∅ ∈ 𝐷 )
26 onsucss ⊢ ( 𝐷 ∈ On → ( ∅ ∈ 𝐷 → suc ∅ ⊆ 𝐷 ) )
27 21 25 26 sylc ⊢ ( ( 𝐷 ∈ On ∧ ¬ 𝐷 = ∅ ) → suc ∅ ⊆ 𝐷 )
28 20 27 eqsstrid ⊢ ( ( 𝐷 ∈ On ∧ ¬ 𝐷 = ∅ ) → 1o ⊆ 𝐷 )
29 28 ex ⊢ ( 𝐷 ∈ On → ( ¬ 𝐷 = ∅ → 1o ⊆ 𝐷 ) )
30 29 adantl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( ¬ 𝐷 = ∅ → 1o ⊆ 𝐷 ) )
31 30 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ¬ 𝐷 = ∅ → 1o ⊆ 𝐷 ) )
32 simpr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → 1o ⊆ 𝐷 )
33 0lt1o ⊢ ∅ ∈ 1o
34 33 a1i ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ∅ ∈ 1o )
35 32 34 sseldd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ∅ ∈ 𝐷 )
36 oaord1 ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( ∅ ∈ 𝐷 ↔ 𝐶 ∈ ( 𝐶 +o 𝐷 ) ) )
37 36 ad2antlr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( ∅ ∈ 𝐷 ↔ 𝐶 ∈ ( 𝐶 +o 𝐷 ) ) )
38 35 37 mpbid ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → 𝐶 ∈ ( 𝐶 +o 𝐷 ) )
39 ssidd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → 𝐶 ⊆ 𝐶 )
40 oacl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 +o 𝐷 ) ∈ On )
41 eloni ⊢ ( ( 𝐶 +o 𝐷 ) ∈ On → Ord ( 𝐶 +o 𝐷 ) )
42 40 41 syl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord ( 𝐶 +o 𝐷 ) )
43 eloni ⊢ ( 𝐶 ∈ On → Ord 𝐶 )
44 43 adantr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → Ord 𝐶 )
45 42 44 jca ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) )
46 45 ad2antlr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) )
47 ordeldif ⊢ ( ( Ord ( 𝐶 +o 𝐷 ) ∧ Ord 𝐶 ) → ( 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝐶 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝐶 ) ) )
48 46 47 syl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ ( 𝐶 ∈ ( 𝐶 +o 𝐷 ) ∧ 𝐶 ⊆ 𝐶 ) ) )
49 38 39 48 mpbir2and ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) )
50 simpl ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → 𝐶 ∈ On )
51 50 ad2antlr ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → 𝐶 ∈ On )
52 oa0 ⊢ ( 𝐶 ∈ On → ( 𝐶 +o ∅ ) = 𝐶 )
53 51 52 syl ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( 𝐶 +o ∅ ) = 𝐶 )
54 53 eqcomd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → 𝐶 = ( 𝐶 +o ∅ ) )
55 eqidd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ ∅ ) )
56 54 55 jca ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( 𝐶 = ( 𝐶 +o ∅ ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ ∅ ) ) )
57 oveq2 ⊢ ( 𝑧 = ∅ → ( 𝐶 +o 𝑧 ) = ( 𝐶 +o ∅ ) )
58 57 eqeq2d ⊢ ( 𝑧 = ∅ → ( 𝐶 = ( 𝐶 +o 𝑧 ) ↔ 𝐶 = ( 𝐶 +o ∅ ) ) )
59 fveq2 ⊢ ( 𝑧 = ∅ → ( 𝐵 ‘ 𝑧 ) = ( 𝐵 ‘ ∅ ) )
60 59 eqeq2d ⊢ ( 𝑧 = ∅ → ( ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ↔ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ ∅ ) ) )
61 58 60 anbi12d ⊢ ( 𝑧 = ∅ → ( ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝐶 = ( 𝐶 +o ∅ ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ ∅ ) ) ) )
62 61 rspcev ⊢ ( ( ∅ ∈ 𝐷 ∧ ( 𝐶 = ( 𝐶 +o ∅ ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ ∅ ) ) ) → ∃ 𝑧 ∈ 𝐷 ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) )
63 35 56 62 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ∃ 𝑧 ∈ 𝐷 ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) )
64 fvexd ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( 𝐵 ‘ ∅ ) ∈ V )
65 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) )
66 65 adantr ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑦 = ( 𝐵 ‘ ∅ ) ) → ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ↔ 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ) )
67 eqeq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 = ( 𝐶 +o 𝑧 ) ↔ 𝐶 = ( 𝐶 +o 𝑧 ) ) )
68 eqeq1 ⊢ ( 𝑦 = ( 𝐵 ‘ ∅ ) → ( 𝑦 = ( 𝐵 ‘ 𝑧 ) ↔ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) )
69 67 68 bi2anan9 ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑦 = ( 𝐵 ‘ ∅ ) ) → ( ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) ) )
70 69 rexbidv ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑦 = ( 𝐵 ‘ ∅ ) ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) ) )
71 66 70 anbi12d ⊢ ( ( 𝑥 = 𝐶 ∧ 𝑦 = ( 𝐵 ‘ ∅ ) ) → ( ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) ↔ ( 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) ) ) )
72 71 opelopabga ⊢ ( ( 𝐶 ∈ On ∧ ( 𝐵 ‘ ∅ ) ∈ V ) → ( ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ↔ ( 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) ) ) )
73 51 64 72 syl2anc ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ( ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ↔ ( 𝐶 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝐶 = ( 𝐶 +o 𝑧 ) ∧ ( 𝐵 ‘ ∅ ) = ( 𝐵 ‘ 𝑧 ) ) ) ) )
74 49 63 73 mpbir2and ⊢ ( ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) ∧ 1o ⊆ 𝐷 ) → ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } )
75 74 ex ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 1o ⊆ 𝐷 → ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
76 ordirr ⊢ ( Ord 𝐶 → ¬ 𝐶 ∈ 𝐶 )
77 43 76 syl ⊢ ( 𝐶 ∈ On → ¬ 𝐶 ∈ 𝐶 )
78 77 adantr ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ¬ 𝐶 ∈ 𝐶 )
79 78 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ¬ 𝐶 ∈ 𝐶 )
80 fndm ⊢ ( 𝐴 Fn 𝐶 → dom 𝐴 = 𝐶 )
81 80 adantr ⊢ ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) → dom 𝐴 = 𝐶 )
82 81 adantr ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → dom 𝐴 = 𝐶 )
83 79 82 neleqtrrd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ¬ 𝐶 ∈ dom 𝐴 )
84 50 adantl ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐶 ∈ On )
85 fvexd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 ‘ ∅ ) ∈ V )
86 84 85 opeldmd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ 𝐴 → 𝐶 ∈ dom 𝐴 ) )
87 83 86 mtod ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ¬ ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ 𝐴 )
88 75 87 jctird ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 1o ⊆ 𝐷 → ( ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ∧ ¬ ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ 𝐴 ) ) )
89 nelss ⊢ ( ( ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ∧ ¬ ⟨ 𝐶 , ( 𝐵 ‘ ∅ ) ⟩ ∈ 𝐴 ) → ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 )
90 88 89 syl6 ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 1o ⊆ 𝐷 → ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 ) )
91 31 90 syld ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ¬ 𝐷 = ∅ → ¬ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 ) )
92 19 91 impcon4bid ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐷 = ∅ ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 ) )
93 8 92 bitrd ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 = ∅ ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 ) )
94 ssequn2 ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ⊆ 𝐴 ↔ ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = 𝐴 )
95 93 94 bitrdi ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 = ∅ ↔ ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = 𝐴 ) )
96 1 tfsconcatun ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 + 𝐵 ) = ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) )
97 96 eqeq1d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 + 𝐵 ) = 𝐴 ↔ ( 𝐴 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐶 +o 𝐷 ) ∖ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐷 ( 𝑥 = ( 𝐶 +o 𝑧 ) ∧ 𝑦 = ( 𝐵 ‘ 𝑧 ) ) ) } ) = 𝐴 ) )
98 95 97 bitr4d ⊢ ( ( ( 𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷 ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 = ∅ ↔ ( 𝐴 + 𝐵 ) = 𝐴 ) )