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 ) ) → ( 𝐴 = ∅ → ( 𝐴 + 𝐵 ) = 𝐵 ) ) |