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→ACBD:AB⟶CD

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=ifA∈VA∅→A≠B↔ifA∈VA∅≠B
8 opeq1 ⊢A=ifA∈VA∅→AC=ifA∈VA∅C
9 8 preq1d ⊢A=ifA∈VA∅→ACBD=ifA∈VA∅CBD
10 preq1 ⊢A=ifA∈VA∅→AB=ifA∈VA∅B
11 9 10 feq12d ⊢A=ifA∈VA∅→ACBD:AB⟶CD↔ifA∈VA∅CBD:ifA∈VA∅B⟶CD
12 7 11 imbi12d ⊢A=ifA∈VA∅→A≠B→ACBD:AB⟶CD↔ifA∈VA∅≠B→ifA∈VA∅CBD:ifA∈VA∅B⟶CD
13 neeq2 ⊢B=ifB∈VB∅→ifA∈VA∅≠B↔ifA∈VA∅≠ifB∈VB∅
14 opeq1 ⊢B=ifB∈VB∅→BD=ifB∈VB∅D
15 14 preq2d ⊢B=ifB∈VB∅→ifA∈VA∅CBD=ifA∈VA∅CifB∈VB∅D
16 preq2 ⊢B=ifB∈VB∅→ifA∈VA∅B=ifA∈VA∅ifB∈VB∅
17 15 16 feq12d ⊢B=ifB∈VB∅→ifA∈VA∅CBD:ifA∈VA∅B⟶CD↔ifA∈VA∅CifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶CD
18 13 17 imbi12d ⊢B=ifB∈VB∅→ifA∈VA∅≠B→ifA∈VA∅CBD:ifA∈VA∅B⟶CD↔ifA∈VA∅≠ifB∈VB∅→ifA∈VA∅CifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶CD
19 opeq2 ⊢C=ifC∈VC∅→ifA∈VA∅C=ifA∈VA∅ifC∈VC∅
20 19 preq1d ⊢C=ifC∈VC∅→ifA∈VA∅CifB∈VB∅D=ifA∈VA∅ifC∈VC∅ifB∈VB∅D
21 eqidd ⊢C=ifC∈VC∅→ifA∈VA∅ifB∈VB∅=ifA∈VA∅ifB∈VB∅
22 preq1 ⊢C=ifC∈VC∅→CD=ifC∈VC∅D
23 20 21 22 feq123d ⊢C=ifC∈VC∅→ifA∈VA∅CifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶CD↔ifA∈VA∅ifC∈VC∅ifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶ifC∈VC∅D
24 23 imbi2d ⊢C=ifC∈VC∅→ifA∈VA∅≠ifB∈VB∅→ifA∈VA∅CifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶CD↔ifA∈VA∅≠ifB∈VB∅→ifA∈VA∅ifC∈VC∅ifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶ifC∈VC∅D
25 opeq2 ⊢D=ifD∈VD∅→ifB∈VB∅D=ifB∈VB∅ifD∈VD∅
26 25 preq2d ⊢D=ifD∈VD∅→ifA∈VA∅ifC∈VC∅ifB∈VB∅D=ifA∈VA∅ifC∈VC∅ifB∈VB∅ifD∈VD∅
27 eqidd ⊢D=ifD∈VD∅→ifA∈VA∅ifB∈VB∅=ifA∈VA∅ifB∈VB∅
28 preq2 ⊢D=ifD∈VD∅→ifC∈VC∅D=ifC∈VC∅ifD∈VD∅
29 26 27 28 feq123d ⊢D=ifD∈VD∅→ifA∈VA∅ifC∈VC∅ifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶ifC∈VC∅D↔ifA∈VA∅ifC∈VC∅ifB∈VB∅ifD∈VD∅:ifA∈VA∅ifB∈VB∅⟶ifC∈VC∅ifD∈VD∅
30 29 imbi2d ⊢D=ifD∈VD∅→ifA∈VA∅≠ifB∈VB∅→ifA∈VA∅ifC∈VC∅ifB∈VB∅D:ifA∈VA∅ifB∈VB∅⟶ifC∈VC∅D↔ifA∈VA∅≠ifB∈VB∅→ifA∈VA∅ifC∈VC∅ifB∈VB∅ifD∈VD∅:ifA∈VA∅ifB∈VB∅⟶ifC∈VC∅ifD∈VD∅
31 0ex ⊢∅∈V
32 31 elimel ⊢ifA∈VA∅∈V
33 31 elimel ⊢ifB∈VB∅∈V
34 31 elimel ⊢ifC∈VC∅∈V
35 31 elimel ⊢ifD∈VD∅∈V
36 32 33 34 35 fpr ⊢ifA∈VA∅≠ifB∈VB∅→ifA∈VA∅ifC∈VC∅ifB∈VB∅ifD∈VD∅:ifA∈VA∅ifB∈VB∅⟶ifC∈VC∅ifD∈VD∅
37 12 18 24 30 36 dedth4h ⊢A∈V∧B∈V∧C∈V∧D∈V→A≠B→ACBD:AB⟶CD
38 3 6 37 syl2an ⊢A∈E∧B∈F∧C∈G∧D∈H→A≠B→ACBD:AB⟶CD
39 38 3impia ⊢A∈E∧B∈F∧C∈G∧D∈H∧A≠B→ACBD:AB⟶CD