Metamath Proof Explorer

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 ⊢ φ → F ∈ V
frege129d.a ⊢ φ → A ∈ dom ⁡ F
frege129d.c ⊢ φ → C = F ⁡ A
frege129d.or ⊢ φ → A t+ ⁡ F B ∨ A = B ∨ B t+ ⁡ F A
frege129d.fun ⊢ φ → Fun ⁡ F
Assertion frege129d ⊢ φ → B t+ ⁡ F C ∨ B = C ∨ C t+ ⁡ F B

Proof

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