Metamath Proof Explorer

Theorem fprg

Description: A function with a domain of two elements. (Contributed by FL, 2-Feb-2014)

Ref Expression
Assertion fprg ⊢ A ∈ E ∧ B ∈ F ∧ C ∈ G ∧ D ∈ H ∧ A ≠ B → A C B D : A B ⟶ C D

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ E → A ∈ V
2 elex ⊢ B ∈ F → B ∈ V
3 1 2 anim12i ⊢ A ∈ E ∧ B ∈ F → A ∈ V ∧ B ∈ V
4 elex ⊢ C ∈ G → C ∈ V
5 elex ⊢ D ∈ H → D ∈ V
6 4 5 anim12i ⊢ C ∈ G ∧ D ∈ H → C ∈ V ∧ D ∈ V
7 neeq1 ⊢ A = if A ∈ V A ∅ → A ≠ B ↔ if A ∈ V A ∅ ≠ B
8 opeq1 ⊢ A = if A ∈ V A ∅ → A C = if A ∈ V A ∅ C
9 8 preq1d ⊢ A = if A ∈ V A ∅ → A C B D = if A ∈ V A ∅ C B D
10 preq1 ⊢ A = if A ∈ V A ∅ → A B = if A ∈ V A ∅ B
11 9 10 feq12d ⊢ A = if A ∈ V A ∅ → A C B D : A B ⟶ C D ↔ if A ∈ V A ∅ C B D : if A ∈ V A ∅ B ⟶ C D
12 7 11 imbi12d ⊢ A = if A ∈ V A ∅ → A ≠ B → A C B D : A B ⟶ C D ↔ if A ∈ V A ∅ ≠ B → if A ∈ V A ∅ C B D : if A ∈ V A ∅ B ⟶ C D
13 neeq2 ⊢ B = if B ∈ V B ∅ → if A ∈ V A ∅ ≠ B ↔ if A ∈ V A ∅ ≠ if B ∈ V B ∅
14 opeq1 ⊢ B = if B ∈ V B ∅ → B D = if B ∈ V B ∅ D
15 14 preq2d ⊢ B = if B ∈ V B ∅ → if A ∈ V A ∅ C B D = if A ∈ V A ∅ C if B ∈ V B ∅ D
16 preq2 ⊢ B = if B ∈ V B ∅ → if A ∈ V A ∅ B = if A ∈ V A ∅ if B ∈ V B ∅
17 15 16 feq12d ⊢ B = if B ∈ V B ∅ → if A ∈ V A ∅ C B D : if A ∈ V A ∅ B ⟶ C D ↔ if A ∈ V A ∅ C if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ C D
18 13 17 imbi12d ⊢ B = if B ∈ V B ∅ → if A ∈ V A ∅ ≠ B → if A ∈ V A ∅ C B D : if A ∈ V A ∅ B ⟶ C D ↔ if A ∈ V A ∅ ≠ if B ∈ V B ∅ → if A ∈ V A ∅ C if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ C D
19 opeq2 ⊢ C = if C ∈ V C ∅ → if A ∈ V A ∅ C = if A ∈ V A ∅ if C ∈ V C ∅
20 19 preq1d ⊢ C = if C ∈ V C ∅ → if A ∈ V A ∅ C if B ∈ V B ∅ D = if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ D
21 eqidd ⊢ C = if C ∈ V C ∅ → if A ∈ V A ∅ if B ∈ V B ∅ = if A ∈ V A ∅ if B ∈ V B ∅
22 preq1 ⊢ C = if C ∈ V C ∅ → C D = if C ∈ V C ∅ D
23 20 21 22 feq123d ⊢ C = if C ∈ V C ∅ → if A ∈ V A ∅ C if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ C D ↔ if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ if C ∈ V C ∅ D
24 23 imbi2d ⊢ C = if C ∈ V C ∅ → if A ∈ V A ∅ ≠ if B ∈ V B ∅ → if A ∈ V A ∅ C if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ C D ↔ if A ∈ V A ∅ ≠ if B ∈ V B ∅ → if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ if C ∈ V C ∅ D
25 opeq2 ⊢ D = if D ∈ V D ∅ → if B ∈ V B ∅ D = if B ∈ V B ∅ if D ∈ V D ∅
26 25 preq2d ⊢ D = if D ∈ V D ∅ → if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ D = if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ if D ∈ V D ∅
27 eqidd ⊢ D = if D ∈ V D ∅ → if A ∈ V A ∅ if B ∈ V B ∅ = if A ∈ V A ∅ if B ∈ V B ∅
28 preq2 ⊢ D = if D ∈ V D ∅ → if C ∈ V C ∅ D = if C ∈ V C ∅ if D ∈ V D ∅
29 26 27 28 feq123d ⊢ D = if D ∈ V D ∅ → if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ if C ∈ V C ∅ D ↔ if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ if D ∈ V D ∅ : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ if C ∈ V C ∅ if D ∈ V D ∅
30 29 imbi2d ⊢ D = if D ∈ V D ∅ → if A ∈ V A ∅ ≠ if B ∈ V B ∅ → if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ D : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ if C ∈ V C ∅ D ↔ if A ∈ V A ∅ ≠ if B ∈ V B ∅ → if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ if D ∈ V D ∅ : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ if C ∈ V C ∅ if D ∈ V D ∅
31 0ex ⊢ ∅ ∈ V
32 31 elimel ⊢ if A ∈ V A ∅ ∈ V
33 31 elimel ⊢ if B ∈ V B ∅ ∈ V
34 31 elimel ⊢ if C ∈ V C ∅ ∈ V
35 31 elimel ⊢ if D ∈ V D ∅ ∈ V
36 32 33 34 35 fpr ⊢ if A ∈ V A ∅ ≠ if B ∈ V B ∅ → if A ∈ V A ∅ if C ∈ V C ∅ if B ∈ V B ∅ if D ∈ V D ∅ : if A ∈ V A ∅ if B ∈ V B ∅ ⟶ if C ∈ V C ∅ if D ∈ V D ∅
37 12 18 24 30 36 dedth4h ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → A ≠ B → A C B D : A B ⟶ C D
38 3 6 37 syl2an ⊢ A ∈ E ∧ B ∈ F ∧ C ∈ G ∧ D ∈ H → A ≠ B → A C B D : A B ⟶ C D
39 38 3impia ⊢ A ∈ E ∧ B ∈ F ∧ C ∈ G ∧ D ∈ H ∧ A ≠ B → A C B D : A B ⟶ C D