Step |
Hyp |
Ref |
Expression |
1 |
|
weiun.1 |
⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) ) |
2 |
|
weiun.2 |
⊢ 𝑇 = { 〈 𝑦 , 𝑧 〉 ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } |
3 |
|
simpl |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → 𝑦 = 𝐶 ) |
4 |
3
|
fveq2d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐶 ) ) |
5 |
|
simpr |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → 𝑧 = 𝐷 ) |
6 |
5
|
fveq2d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐷 ) ) |
7 |
4 6
|
breq12d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐶 ) 𝑅 ( 𝐹 ‘ 𝐷 ) ) ) |
8 |
4 6
|
eqeq12d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ) ) |
9 |
4
|
csbeq1d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 ) |
10 |
3 9 5
|
breq123d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) |
11 |
8 10
|
anbi12d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ∧ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) ) |
12 |
7 11
|
orbi12d |
⊢ ( ( 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝐶 ) 𝑅 ( 𝐹 ‘ 𝐷 ) ∨ ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ∧ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) ) ) |
13 |
12 2
|
brab2a |
⊢ ( 𝐶 𝑇 𝐷 ↔ ( ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐷 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝐶 ) 𝑅 ( 𝐹 ‘ 𝐷 ) ∨ ( ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐷 ) ∧ 𝐶 ⦋ ( 𝐹 ‘ 𝐶 ) / 𝑥 ⦌ 𝑆 𝐷 ) ) ) ) |