Metamath Proof Explorer

Theorem relexp0eq

Description: The zeroth power of relationships is the same if and only if the union of their domain and ranges is the same. (Contributed by RP, 11-Jun-2020)

Ref Expression
Assertion relexp0eq ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ( 𝐴 ↑𝑟 0 ) = ( 𝐵 ↑𝑟 0 ) ) )

Proof

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 ) ) )