Step |
Hyp |
Ref |
Expression |
1 |
|
dfcleq |
⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
2 |
|
alcom |
⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
3 |
|
19.3v |
⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
4 |
|
ax6ev |
⊢ ∃ 𝑦 𝑦 = 𝑥 |
5 |
|
pm5.5 |
⊢ ( ∃ 𝑦 𝑦 = 𝑥 → ( ( ∃ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ) |
6 |
4 5
|
ax-mp |
⊢ ( ( ∃ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
7 |
|
19.23v |
⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ∃ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ) |
8 |
|
19.3v |
⊢ ( ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
9 |
6 7 8
|
3bitr4ri |
⊢ ( ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ) |
10 |
|
pm5.32 |
⊢ ( ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ( 𝑦 = 𝑥 ∧ 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ) ↔ ( 𝑦 = 𝑥 ∧ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ) |
11 |
|
ancom |
⊢ ( ( 𝑦 = 𝑥 ∧ 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ) |
12 |
|
ancom |
⊢ ( ( 𝑦 = 𝑥 ∧ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) |
13 |
11 12
|
bibi12i |
⊢ ( ( ( 𝑦 = 𝑥 ∧ 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ) ↔ ( 𝑦 = 𝑥 ∧ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
14 |
10 13
|
bitri |
⊢ ( ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
15 |
14
|
albii |
⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
16 |
9 15
|
bitri |
⊢ ( ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
17 |
16
|
albii |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
18 |
2 3 17
|
3bitr3i |
⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
19 |
1 18
|
bitri |
⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
20 |
|
eqopab2bw |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) } ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) ) |
21 |
|
opabresid |
⊢ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) } |
22 |
21
|
eqcomi |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) } = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) |
23 |
|
opabresid |
⊢ ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) } |
24 |
23
|
eqcomi |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) } = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) |
25 |
22 24
|
eqeq12i |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) } ↔ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
26 |
19 20 25
|
3bitr2i |
⊢ ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
27 |
|
relexp0g |
⊢ ( 𝐴 ∈ 𝑈 → ( 𝐴 ↑𝑟 0 ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) |
28 |
|
relexp0g |
⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ↑𝑟 0 ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) ) |
29 |
27 28
|
eqeqan12d |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 ↑𝑟 0 ) = ( 𝐵 ↑𝑟 0 ) ↔ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ) |
30 |
26 29
|
bitr4id |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ( 𝐴 ↑𝑟 0 ) = ( 𝐵 ↑𝑟 0 ) ) ) |