Proof of Theorem fprg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elex 3500 | . . . 4
⊢ (𝐴 ∈ 𝐸 → 𝐴 ∈ V) | 
| 2 |  | elex 3500 | . . . 4
⊢ (𝐵 ∈ 𝐹 → 𝐵 ∈ V) | 
| 3 | 1, 2 | anim12i 613 | . . 3
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | 
| 4 |  | elex 3500 | . . . 4
⊢ (𝐶 ∈ 𝐺 → 𝐶 ∈ V) | 
| 5 |  | elex 3500 | . . . 4
⊢ (𝐷 ∈ 𝐻 → 𝐷 ∈ V) | 
| 6 | 4, 5 | anim12i 613 | . . 3
⊢ ((𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) → (𝐶 ∈ V ∧ 𝐷 ∈ V)) | 
| 7 |  | neeq1 3002 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ V, 𝐴, ∅) → (𝐴 ≠ 𝐵 ↔ if(𝐴 ∈ V, 𝐴, ∅) ≠ 𝐵)) | 
| 8 |  | opeq1 4872 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ V, 𝐴, ∅) → 〈𝐴, 𝐶〉 = 〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉) | 
| 9 | 8 | preq1d 4738 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ V, 𝐴, ∅) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈𝐵, 𝐷〉}) | 
| 10 |  | preq1 4732 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ V, 𝐴, ∅) → {𝐴, 𝐵} = {if(𝐴 ∈ V, 𝐴, ∅), 𝐵}) | 
| 11 | 9, 10 | feq12d 6723 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ V, 𝐴, ∅) → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷} ↔ {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈𝐵, 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), 𝐵}⟶{𝐶, 𝐷})) | 
| 12 | 7, 11 | imbi12d 344 | . . . 4
⊢ (𝐴 = if(𝐴 ∈ V, 𝐴, ∅) → ((𝐴 ≠ 𝐵 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) ↔ (if(𝐴 ∈ V, 𝐴, ∅) ≠ 𝐵 → {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈𝐵, 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), 𝐵}⟶{𝐶, 𝐷}))) | 
| 13 |  | neeq2 3003 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ V, 𝐵, ∅) → (if(𝐴 ∈ V, 𝐴, ∅) ≠ 𝐵 ↔ if(𝐴 ∈ V, 𝐴, ∅) ≠ if(𝐵 ∈ V, 𝐵, ∅))) | 
| 14 |  | opeq1 4872 | . . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ V, 𝐵, ∅) → 〈𝐵, 𝐷〉 = 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉) | 
| 15 | 14 | preq2d 4739 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ V, 𝐵, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈𝐵, 𝐷〉} = {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}) | 
| 16 |  | preq2 4733 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ V, 𝐵, ∅) → {if(𝐴 ∈ V, 𝐴, ∅), 𝐵} = {if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}) | 
| 17 | 15, 16 | feq12d 6723 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ V, 𝐵, ∅) → ({〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈𝐵, 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), 𝐵}⟶{𝐶, 𝐷} ↔ {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{𝐶, 𝐷})) | 
| 18 | 13, 17 | imbi12d 344 | . . . 4
⊢ (𝐵 = if(𝐵 ∈ V, 𝐵, ∅) → ((if(𝐴 ∈ V, 𝐴, ∅) ≠ 𝐵 → {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈𝐵, 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), 𝐵}⟶{𝐶, 𝐷}) ↔ (if(𝐴 ∈ V, 𝐴, ∅) ≠ if(𝐵 ∈ V, 𝐵, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{𝐶, 𝐷}))) | 
| 19 |  | opeq2 4873 | . . . . . . 7
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → 〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉 = 〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉) | 
| 20 | 19 | preq1d 4738 | . . . . . 6
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉} = {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}) | 
| 21 |  | eqidd 2737 | . . . . . 6
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → {if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)} = {if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}) | 
| 22 |  | preq1 4732 | . . . . . 6
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → {𝐶, 𝐷} = {if(𝐶 ∈ V, 𝐶, ∅), 𝐷}) | 
| 23 | 20, 21, 22 | feq123d 6724 | . . . . 5
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → ({〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{𝐶, 𝐷} ↔ {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{if(𝐶 ∈ V, 𝐶, ∅), 𝐷})) | 
| 24 | 23 | imbi2d 340 | . . . 4
⊢ (𝐶 = if(𝐶 ∈ V, 𝐶, ∅) → ((if(𝐴 ∈ V, 𝐴, ∅) ≠ if(𝐵 ∈ V, 𝐵, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), 𝐶〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{𝐶, 𝐷}) ↔ (if(𝐴 ∈ V, 𝐴, ∅) ≠ if(𝐵 ∈ V, 𝐵, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{if(𝐶 ∈ V, 𝐶, ∅), 𝐷}))) | 
| 25 |  | opeq2 4873 | . . . . . . 7
⊢ (𝐷 = if(𝐷 ∈ V, 𝐷, ∅) → 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉 = 〈if(𝐵 ∈ V, 𝐵, ∅), if(𝐷 ∈ V, 𝐷, ∅)〉) | 
| 26 | 25 | preq2d 4739 | . . . . . 6
⊢ (𝐷 = if(𝐷 ∈ V, 𝐷, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉} = {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), if(𝐷 ∈ V, 𝐷, ∅)〉}) | 
| 27 |  | eqidd 2737 | . . . . . 6
⊢ (𝐷 = if(𝐷 ∈ V, 𝐷, ∅) → {if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)} = {if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}) | 
| 28 |  | preq2 4733 | . . . . . 6
⊢ (𝐷 = if(𝐷 ∈ V, 𝐷, ∅) → {if(𝐶 ∈ V, 𝐶, ∅), 𝐷} = {if(𝐶 ∈ V, 𝐶, ∅), if(𝐷 ∈ V, 𝐷, ∅)}) | 
| 29 | 26, 27, 28 | feq123d 6724 | . . . . 5
⊢ (𝐷 = if(𝐷 ∈ V, 𝐷, ∅) → ({〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{if(𝐶 ∈ V, 𝐶, ∅), 𝐷} ↔ {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), if(𝐷 ∈ V, 𝐷, ∅)〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{if(𝐶 ∈ V, 𝐶, ∅), if(𝐷 ∈ V, 𝐷, ∅)})) | 
| 30 | 29 | imbi2d 340 | . . . 4
⊢ (𝐷 = if(𝐷 ∈ V, 𝐷, ∅) → ((if(𝐴 ∈ V, 𝐴, ∅) ≠ if(𝐵 ∈ V, 𝐵, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), 𝐷〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{if(𝐶 ∈ V, 𝐶, ∅), 𝐷}) ↔ (if(𝐴 ∈ V, 𝐴, ∅) ≠ if(𝐵 ∈ V, 𝐵, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), if(𝐷 ∈ V, 𝐷, ∅)〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{if(𝐶 ∈ V, 𝐶, ∅), if(𝐷 ∈ V, 𝐷, ∅)}))) | 
| 31 |  | 0ex 5306 | . . . . . 6
⊢ ∅
∈ V | 
| 32 | 31 | elimel 4594 | . . . . 5
⊢ if(𝐴 ∈ V, 𝐴, ∅) ∈ V | 
| 33 | 31 | elimel 4594 | . . . . 5
⊢ if(𝐵 ∈ V, 𝐵, ∅) ∈ V | 
| 34 | 31 | elimel 4594 | . . . . 5
⊢ if(𝐶 ∈ V, 𝐶, ∅) ∈ V | 
| 35 | 31 | elimel 4594 | . . . . 5
⊢ if(𝐷 ∈ V, 𝐷, ∅) ∈ V | 
| 36 | 32, 33, 34, 35 | fpr 7173 | . . . 4
⊢ (if(𝐴 ∈ V, 𝐴, ∅) ≠ if(𝐵 ∈ V, 𝐵, ∅) → {〈if(𝐴 ∈ V, 𝐴, ∅), if(𝐶 ∈ V, 𝐶, ∅)〉, 〈if(𝐵 ∈ V, 𝐵, ∅), if(𝐷 ∈ V, 𝐷, ∅)〉}:{if(𝐴 ∈ V, 𝐴, ∅), if(𝐵 ∈ V, 𝐵, ∅)}⟶{if(𝐶 ∈ V, 𝐶, ∅), if(𝐷 ∈ V, 𝐷, ∅)}) | 
| 37 | 12, 18, 24, 30, 36 | dedth4h 4586 | . . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐶 ∈ V ∧ 𝐷 ∈ V)) → (𝐴 ≠ 𝐵 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷})) | 
| 38 | 3, 6, 37 | syl2an 596 | . 2
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻)) → (𝐴 ≠ 𝐵 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷})) | 
| 39 | 38 | 3impia 1117 | 1
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) |