| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ov 7434 | . . . . 5
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | 
| 2 |  | ovg.5 | . . . . . 6
⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} | 
| 3 | 2 | fveq1i 6907 | . . . . 5
⊢ (𝐹‘〈𝐴, 𝐵〉) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) | 
| 4 | 1, 3 | eqtri 2765 | . . . 4
⊢ (𝐴𝐹𝐵) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) | 
| 5 | 4 | eqeq1i 2742 | . . 3
⊢ ((𝐴𝐹𝐵) = 𝐶 ↔ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶) | 
| 6 |  | eqeq2 2749 | . . . . . . . . . 10
⊢ (𝑐 = 𝐶 → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝑐 ↔ ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶)) | 
| 7 |  | opeq2 4874 | . . . . . . . . . . 11
⊢ (𝑐 = 𝐶 → 〈〈𝐴, 𝐵〉, 𝑐〉 = 〈〈𝐴, 𝐵〉, 𝐶〉) | 
| 8 | 7 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑐 = 𝐶 → (〈〈𝐴, 𝐵〉, 𝑐〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})) | 
| 9 | 6, 8 | bibi12d 345 | . . . . . . . . 9
⊢ (𝑐 = 𝐶 → ((({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝑐 ↔ 〈〈𝐴, 𝐵〉, 𝑐〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}) ↔ (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}))) | 
| 10 | 9 | imbi2d 340 | . . . . . . . 8
⊢ (𝑐 = 𝐶 → (((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝑐 ↔ 〈〈𝐴, 𝐵〉, 𝑐〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})) ↔ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})))) | 
| 11 |  | ovg.4 | . . . . . . . . . . . 12
⊢ ((𝜏 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)) → ∃!𝑧𝜑) | 
| 12 | 11 | ex 412 | . . . . . . . . . . 11
⊢ (𝜏 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)) | 
| 13 | 12 | alrimivv 1928 | . . . . . . . . . 10
⊢ (𝜏 → ∀𝑥∀𝑦((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑)) | 
| 14 |  | fnoprabg 7556 | . . . . . . . . . 10
⊢
(∀𝑥∀𝑦((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) → ∃!𝑧𝜑) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} Fn {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)}) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . 9
⊢ (𝜏 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} Fn {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)}) | 
| 16 |  | eleq1 2829 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑅 ↔ 𝐴 ∈ 𝑅)) | 
| 17 | 16 | anbi1d 631 | . . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ↔ (𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆))) | 
| 18 |  | eleq1 2829 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝑆 ↔ 𝐵 ∈ 𝑆)) | 
| 19 | 18 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ↔ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆))) | 
| 20 | 17, 19 | opelopabg 5543 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)} ↔ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆))) | 
| 21 | 20 | ibir 268 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)}) | 
| 22 |  | fnopfvb 6960 | . . . . . . . . 9
⊢
(({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} Fn {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)} ∧ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆)}) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝑐 ↔ 〈〈𝐴, 𝐵〉, 𝑐〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})) | 
| 23 | 15, 21, 22 | syl2an 596 | . . . . . . . 8
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝑐 ↔ 〈〈𝐴, 𝐵〉, 𝑐〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})) | 
| 24 | 10, 23 | vtoclg 3554 | . . . . . . 7
⊢ (𝐶 ∈ 𝐷 → ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}))) | 
| 25 | 24 | com12 32 | . . . . . 6
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐶 ∈ 𝐷 → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}))) | 
| 26 | 25 | exp32 420 | . . . . 5
⊢ (𝜏 → (𝐴 ∈ 𝑅 → (𝐵 ∈ 𝑆 → (𝐶 ∈ 𝐷 → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}))))) | 
| 27 | 26 | 3imp2 1350 | . . . 4
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ 〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)})) | 
| 28 |  | ovg.1 | . . . . . . 7
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| 29 | 17, 28 | anbi12d 632 | . . . . . 6
⊢ (𝑥 = 𝐴 → (((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑) ↔ ((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜓))) | 
| 30 |  | ovg.2 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) | 
| 31 | 19, 30 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = 𝐵 → (((𝐴 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜓) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜒))) | 
| 32 |  | ovg.3 | . . . . . . 7
⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃)) | 
| 33 | 32 | anbi2d 630 | . . . . . 6
⊢ (𝑧 = 𝐶 → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜒) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) | 
| 34 | 29, 31, 33 | eloprabg 7543 | . . . . 5
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) | 
| 35 | 34 | adantl 481 | . . . 4
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → (〈〈𝐴, 𝐵〉, 𝐶〉 ∈ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)} ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) | 
| 36 | 27, 35 | bitrd 279 | . . 3
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → (({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆) ∧ 𝜑)}‘〈𝐴, 𝐵〉) = 𝐶 ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) | 
| 37 | 5, 36 | bitrid 283 | . 2
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) | 
| 38 |  | biidd 262 | . . . . 5
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃))) | 
| 39 | 38 | bianabs 541 | . . . 4
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃) ↔ 𝜃)) | 
| 40 | 39 | 3adant3 1133 | . . 3
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷) → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃) ↔ 𝜃)) | 
| 41 | 40 | adantl 481 | . 2
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝜃) ↔ 𝜃)) | 
| 42 | 37, 41 | bitrd 279 | 1
⊢ ((𝜏 ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝐷)) → ((𝐴𝐹𝐵) = 𝐶 ↔ 𝜃)) |