Theorem frege129d

Description: If F is a function and (for distinct A and B ) either A follows B or B follows A in the transitive closure of F , the successor of A is either B or it follows B or it comes before B in the transitive closure of F . Similar to Proposition 129 of Frege1879 p. 83. Comparw with frege129 . (Contributed by RP, 16-Jul-2020)

	Ref	Expression
Hypotheses	frege129d.f	⊢ ( 𝜑 → 𝐹 ∈ V )
	frege129d.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝐹 )
	frege129d.c	⊢ ( 𝜑 → 𝐶 = ( 𝐹 ‘ 𝐴 ) )
	frege129d.or	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )
	frege129d.fun	⊢ ( 𝜑 → Fun 𝐹 )
Assertion	frege129d	⊢ ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		frege129d.f	⊢ ( 𝜑 → 𝐹 ∈ V )
2		frege129d.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝐹 )
3		frege129d.c	⊢ ( 𝜑 → 𝐶 = ( 𝐹 ‘ 𝐴 ) )
4		frege129d.or	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )
5		frege129d.fun	⊢ ( 𝜑 → Fun 𝐹 )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐹 ∈ V )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐴 ∈ dom 𝐹 )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐶 = ( 𝐹 ‘ 𝐴 ) )
9		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → 𝐴 ( t+ ‘ 𝐹 ) 𝐵 )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → Fun 𝐹 )
11	6 7 8 9 10	frege126d	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐶 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
12		biid	⊢ ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ↔ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 )
13		eqcom	⊢ ( 𝐶 = 𝐵 ↔ 𝐵 = 𝐶 )
14		biid	⊢ ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ↔ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 )
15	12 13 14	3orbi123i	⊢ ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐶 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) ↔ ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
16	11 15	sylib	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
17		3orcomb	⊢ ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) ↔ ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ) )
18		3orrot	⊢ ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ) ↔ ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
19	17 18	sylbb	⊢ ( ( 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐵 = 𝐶 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
20	16 19	syl	⊢ ( ( 𝜑 ∧ 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ) → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
21	20	ex	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
22		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
23	3	eqcomd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
24		funbrfvb	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐶 ↔ 𝐴 𝐹 𝐶 ) )
25	24	biimpd	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐶 → 𝐴 𝐹 𝐶 ) )
26	5 2 25	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = 𝐶 → 𝐴 𝐹 𝐶 ) )
27	23 26	mpd	⊢ ( 𝜑 → 𝐴 𝐹 𝐶 )
28	1 27	frege91d	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝐹 ) 𝐶 )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ( t+ ‘ 𝐹 ) 𝐶 )
30	22 29	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 ( t+ ‘ 𝐹 ) 𝐶 )
31	30	ex	⊢ ( 𝜑 → ( 𝐴 = 𝐵 → 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
32		3mix1	⊢ ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )
33	31 32	syl6	⊢ ( 𝜑 → ( 𝐴 = 𝐵 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
34	1	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐹 ∈ V )
35		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
36	5 35	syl	⊢ ( 𝜑 → Rel 𝐹 )
37		reltrclfv	⊢ ( ( 𝐹 ∈ V ∧ Rel 𝐹 ) → Rel ( t+ ‘ 𝐹 ) )
38	1 36 37	syl2anc	⊢ ( 𝜑 → Rel ( t+ ‘ 𝐹 ) )
39		brrelex1	⊢ ( ( Rel ( t+ ‘ 𝐹 ) ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ∈ V )
40	38 39	sylan	⊢ ( ( 𝜑 ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ∈ V )
41		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
42	3 41	eqeltrdi	⊢ ( 𝜑 → 𝐶 ∈ V )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐶 ∈ V )
44	2	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐴 ∈ V )
46		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ( t+ ‘ 𝐹 ) 𝐴 )
47	27	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐴 𝐹 𝐶 )
48	34 40 43 45 46 47	frege96d	⊢ ( ( 𝜑 ∧ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → 𝐵 ( t+ ‘ 𝐹 ) 𝐶 )
49	48	ex	⊢ ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐴 → 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ) )
50	49 32	syl6	⊢ ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐴 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
51	21 33 50	3jaod	⊢ ( 𝜑 → ( ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) ) )
52	4 51	mpd	⊢ ( 𝜑 → ( 𝐵 ( t+ ‘ 𝐹 ) 𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶 ( t+ ‘ 𝐹 ) 𝐵 ) )