Metamath Proof Explorer

Theorem frege77d

Description: If the images of both { A } and U are subsets of U and B follows A in the transitive closure of R , then B is an element of U . Similar to Proposition 77 of Frege1879 p. 62. Compare with frege77 . (Contributed by RP, 15-Jul-2020)

		Ref	Expression
	Hypotheses	frege77d.r	$⊢ φ \to R \in V$
		frege77d.a	$⊢ φ \to A \in V$
		frege77d.b	$⊢ φ \to B \in V$
		frege77d.ab	$⊢ φ \to A t+ (R) B$
		frege77d.he	$⊢ φ \to R [U] \subseteq U$
		frege77d.ss	$⊢ φ \to R [\{A\}] \subseteq U$
	Assertion	frege77d	$⊢ φ \to B \in U$

Proof

Step	Hyp	Ref	Expression
1		frege77d.r	$⊢ φ \to R \in V$
2		frege77d.a	$⊢ φ \to A \in V$
3		frege77d.b	$⊢ φ \to B \in V$
4		frege77d.ab	$⊢ φ \to A t+ (R) B$
5		frege77d.he	$⊢ φ \to R [U] \subseteq U$
6		frege77d.ss	$⊢ φ \to R [\{A\}] \subseteq U$
7		imaundi	$⊢ R [\{A\} \cup U] = R [\{A\}] \cup R [U]$
8	6 5	unssd	$⊢ φ \to R [\{A\}] \cup R [U] \subseteq U$
9	7 8	eqsstrid	$⊢ φ \to R [\{A\} \cup U] \subseteq U$
10		trclimalb2	$⊢ (R \in V \land R [\{A\} \cup U] \subseteq U) \to t+ (R) [\{A\}] \subseteq U$
11	1 9 10	syl2anc	$⊢ φ \to t+ (R) [\{A\}] \subseteq U$
12		df-br	$⊢ A t+ (R) B \leftrightarrow ⟨A, B⟩ \in t+ (R)$
13	4 12	sylib	$⊢ φ \to ⟨A, B⟩ \in t+ (R)$
14		elimasng	$⊢ (A \in V \land B \in V) \to (B \in t+ (R) [\{A\}] \leftrightarrow ⟨A, B⟩ \in t+ (R))$
15	2 3 14	syl2anc	$⊢ φ \to (B \in t+ (R) [\{A\}] \leftrightarrow ⟨A, B⟩ \in t+ (R))$
16	13 15	mpbird	$⊢ φ \to B \in t+ (R) [\{A\}]$
17	11 16	sseldd	$⊢ φ \to B \in U$