frege133d

Description: If F is a function and A and B both follow X in the transitive closure of F , then (for distinct A and B ) either A follows B or B follows A in the transitive closure of F (or both if it loops). Similar to Proposition 133 of Frege1879 p. 86. Compare with frege133 . (Contributed by RP, 18-Jul-2020)

	Ref	Expression
Hypotheses	frege133d.f	⊢ ( 𝜑 → 𝐹 ∈ V )
	frege133d.xa	⊢ ( 𝜑 → 𝑋 ( t+ ‘ 𝐹 ) 𝐴 )
	frege133d.xb	⊢ ( 𝜑 → 𝑋 ( t+ ‘ 𝐹 ) 𝐵 )
	frege133d.fun	⊢ ( 𝜑 → Fun 𝐹 )
Assertion	frege133d	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		frege133d.f	⊢ ( 𝜑 → 𝐹 ∈ V )
2		frege133d.xa	⊢ ( 𝜑 → 𝑋 ( t+ ‘ 𝐹 ) 𝐴 )
3		frege133d.xb	⊢ ( 𝜑 → 𝑋 ( t+ ‘ 𝐹 ) 𝐵 )
4		frege133d.fun	⊢ ( 𝜑 → Fun 𝐹 )
5		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
6	4 5	syl	⊢ ( 𝜑 → Rel 𝐹 )
7		reltrclfv	⊢ ( ( 𝐹 ∈ V ∧ Rel 𝐹 ) → Rel ( t+ ‘ 𝐹 ) )
8	1 6 7	syl2anc	⊢ ( 𝜑 → Rel ( t+ ‘ 𝐹 ) )
9		eliniseg2	⊢ ( Rel ( t+ ‘ 𝐹 ) → ( 𝑋 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ↔ 𝑋 ( t+ ‘ 𝐹 ) 𝐵 ) )
10	8 9	syl	⊢ ( 𝜑 → ( 𝑋 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ↔ 𝑋 ( t+ ‘ 𝐹 ) 𝐵 ) )
11	3 10	mpbird	⊢ ( 𝜑 → 𝑋 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) )
12		brrelex2	⊢ ( ( Rel ( t+ ‘ 𝐹 ) ∧ 𝑋 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐴 ∈ V )
13	8 2 12	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ V )
14		un12	⊢ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) = ( { 𝐵 } ∪ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) )
15	14	a1i	⊢ ( 𝜑 → ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) = ( { 𝐵 } ∪ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) )
16	1 15 4	frege131d	⊢ ( 𝜑 → ( 𝐹 “ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) ) ⊆ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) )
17	1 11 13 2 16	frege83d	⊢ ( 𝜑 → 𝐴 ∈ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) )
18		elun	⊢ ( 𝐴 ∈ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ↔ ( 𝐴 ∈ { 𝐵 } ∨ 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) )
19	18	orbi2i	⊢ ( ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ 𝐴 ∈ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) ↔ ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ ( 𝐴 ∈ { 𝐵 } ∨ 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) )
20		elun	⊢ ( 𝐴 ∈ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) ↔ ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ 𝐴 ∈ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) )
21		3orass	⊢ ( ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ 𝐴 ∈ { 𝐵 } ∨ 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ↔ ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ ( 𝐴 ∈ { 𝐵 } ∨ 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) )
22	19 20 21	3bitr4i	⊢ ( 𝐴 ∈ ( ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) ) ↔ ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ 𝐴 ∈ { 𝐵 } ∨ 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) )
23	17 22	sylib	⊢ ( 𝜑 → ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ 𝐴 ∈ { 𝐵 } ∨ 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) )
24		eliniseg2	⊢ ( Rel ( t+ ‘ 𝐹 ) → ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ↔ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) )
25	8 24	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ↔ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) )
26	25	biimpd	⊢ ( 𝜑 → ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) → 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) )
27		elsni	⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 )
28	27	a1i	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 ) )
29		elrelimasn	⊢ ( Rel ( t+ ‘ 𝐹 ) → ( 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ↔ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )
30	8 29	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ↔ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )
31	30	biimpd	⊢ ( 𝜑 → ( 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) → 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )
32	26 28 31	3orim123d	⊢ ( 𝜑 → ( ( 𝐴 ∈ ( ^◡ ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ∨ 𝐴 ∈ { 𝐵 } ∨ 𝐴 ∈ ( ( t+ ‘ 𝐹 ) “ { 𝐵 } ) ) → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) ) )
33	23 32	mpd	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )

Metamath Proof Explorer

Theorem frege133d

Proof