This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipole

Description: Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

		Ref	Expression
	Hypotheses	ipoval.i	$⊢ I = toInc (F)$
		ipole.l	$⊢ \underset{˙}{\leq} = \leq_{I}$
	Assertion	ipole	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \underset{˙}{\leq} Y \leftrightarrow X \subseteq Y)$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$⊢ I = toInc (F)$
2		ipole.l	$⊢ \underset{˙}{\leq} = \leq_{I}$
3		preq12	$⊢ (x = X \land y = Y) \to \{x, y\} = \{X, Y\}$
4	3	sseq1d	$⊢ (x = X \land y = Y) \to (\{x, y\} \subseteq F \leftrightarrow \{X, Y\} \subseteq F)$
5		sseq12	$⊢ (x = X \land y = Y) \to (x \subseteq y \leftrightarrow X \subseteq Y)$
6	4 5	anbi12d	$⊢ (x = X \land y = Y) \to ((\{x, y\} \subseteq F \land x \subseteq y) \leftrightarrow (\{X, Y\} \subseteq F \land X \subseteq Y))$
7		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}$
8	6 7	brabga	$⊢ (X \in F \land Y \in F) \to (X \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} Y \leftrightarrow (\{X, Y\} \subseteq F \land X \subseteq Y))$
9	8	3adant1	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} Y \leftrightarrow (\{X, Y\} \subseteq F \land X \subseteq Y))$
10	1	ipolerval	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \leq_{I}$
11	2 10	eqtr4id	$⊢ F \in V \to \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}$
12	11	breqd	$⊢ F \in V \to (X \underset{˙}{\leq} Y \leftrightarrow X \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} Y)$
13	12	3ad2ant1	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \underset{˙}{\leq} Y \leftrightarrow X \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} Y)$
14		prssi	$⊢ (X \in F \land Y \in F) \to \{X, Y\} \subseteq F$
15	14	3adant1	$⊢ (F \in V \land X \in F \land Y \in F) \to \{X, Y\} \subseteq F$
16	15	biantrurd	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \subseteq Y \leftrightarrow (\{X, Y\} \subseteq F \land X \subseteq Y))$
17	9 13 16	3bitr4d	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \underset{˙}{\leq} Y \leftrightarrow X \subseteq Y)$