infpr

		Ref	Expression
	Assertion	infpr	$⊢ (R Or A \land B \in A \land C \in A) \to sup (\{B, C\}, A, R) = if (B R C, B, C)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (R Or A \land B \in A \land C \in A) \to R Or A$
2		ifcl	$⊢ (B \in A \land C \in A) \to if (B R C, B, C) \in A$
3	2	3adant1	$⊢ (R Or A \land B \in A \land C \in A) \to if (B R C, B, C) \in A$
4		ifpr	$⊢ (B \in A \land C \in A) \to if (B R C, B, C) \in \{B, C\}$
5	4	3adant1	$⊢ (R Or A \land B \in A \land C \in A) \to if (B R C, B, C) \in \{B, C\}$
6		breq2	$⊢ B = if (B R C, B, C) \to (B R B \leftrightarrow B R if (B R C, B, C))$
7	6	notbid	$⊢ B = if (B R C, B, C) \to (\neg B R B \leftrightarrow \neg B R if (B R C, B, C))$
8		breq2	$⊢ C = if (B R C, B, C) \to (B R C \leftrightarrow B R if (B R C, B, C))$
9	8	notbid	$⊢ C = if (B R C, B, C) \to (\neg B R C \leftrightarrow \neg B R if (B R C, B, C))$
10		sonr	$⊢ (R Or A \land B \in A) \to \neg B R B$
11	10	3adant3	$⊢ (R Or A \land B \in A \land C \in A) \to \neg B R B$
12	11	adantr	$⊢ ((R Or A \land B \in A \land C \in A) \land B R C) \to \neg B R B$
13		simpr	$⊢ ((R Or A \land B \in A \land C \in A) \land \neg B R C) \to \neg B R C$
14	7 9 12 13	ifbothda	$⊢ (R Or A \land B \in A \land C \in A) \to \neg B R if (B R C, B, C)$
15		breq2	$⊢ B = if (B R C, B, C) \to (C R B \leftrightarrow C R if (B R C, B, C))$
16	15	notbid	$⊢ B = if (B R C, B, C) \to (\neg C R B \leftrightarrow \neg C R if (B R C, B, C))$
17		breq2	$⊢ C = if (B R C, B, C) \to (C R C \leftrightarrow C R if (B R C, B, C))$
18	17	notbid	$⊢ C = if (B R C, B, C) \to (\neg C R C \leftrightarrow \neg C R if (B R C, B, C))$
19		so2nr	$⊢ (R Or A \land (B \in A \land C \in A)) \to \neg (B R C \land C R B)$
20	19	3impb	$⊢ (R Or A \land B \in A \land C \in A) \to \neg (B R C \land C R B)$
21		imnan	$⊢ (B R C \to \neg C R B) \leftrightarrow \neg (B R C \land C R B)$
22	20 21	sylibr	$⊢ (R Or A \land B \in A \land C \in A) \to (B R C \to \neg C R B)$
23	22	imp	$⊢ ((R Or A \land B \in A \land C \in A) \land B R C) \to \neg C R B$
24		sonr	$⊢ (R Or A \land C \in A) \to \neg C R C$
25	24	3adant2	$⊢ (R Or A \land B \in A \land C \in A) \to \neg C R C$
26	25	adantr	$⊢ ((R Or A \land B \in A \land C \in A) \land \neg B R C) \to \neg C R C$
27	16 18 23 26	ifbothda	$⊢ (R Or A \land B \in A \land C \in A) \to \neg C R if (B R C, B, C)$
28		breq1	$⊢ y = B \to (y R if (B R C, B, C) \leftrightarrow B R if (B R C, B, C))$
29	28	notbid	$⊢ y = B \to (\neg y R if (B R C, B, C) \leftrightarrow \neg B R if (B R C, B, C))$
30		breq1	$⊢ y = C \to (y R if (B R C, B, C) \leftrightarrow C R if (B R C, B, C))$
31	30	notbid	$⊢ y = C \to (\neg y R if (B R C, B, C) \leftrightarrow \neg C R if (B R C, B, C))$
32	29 31	ralprg	$⊢ (B \in A \land C \in A) \to (\forall y \in \{B, C\} \neg y R if (B R C, B, C) \leftrightarrow (\neg B R if (B R C, B, C) \land \neg C R if (B R C, B, C)))$
33	32	3adant1	$⊢ (R Or A \land B \in A \land C \in A) \to (\forall y \in \{B, C\} \neg y R if (B R C, B, C) \leftrightarrow (\neg B R if (B R C, B, C) \land \neg C R if (B R C, B, C)))$
34	14 27 33	mpbir2and	$⊢ (R Or A \land B \in A \land C \in A) \to \forall y \in \{B, C\} \neg y R if (B R C, B, C)$
35	34	r19.21bi	$⊢ ((R Or A \land B \in A \land C \in A) \land y \in \{B, C\}) \to \neg y R if (B R C, B, C)$
36	1 3 5 35	infmin	$⊢ (R Or A \land B \in A \land C \in A) \to sup (\{B, C\}, A, R) = if (B R C, B, C)$

Metamath Proof Explorer

Theorem infpr

Proof