Metamath Proof Explorer

Theorem 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 ⊢ φ → F ∈ V
frege133d.xa ⊢ φ → X t+ ⁡ F A
frege133d.xb ⊢ φ → X t+ ⁡ F B
frege133d.fun ⊢ φ → Fun ⁡ F
Assertion frege133d ⊢ φ → A t+ ⁡ F B ∨ A = B ∨ B t+ ⁡ F A

Proof

Step Hyp Ref Expression
1 frege133d.f ⊢ φ → F ∈ V
2 frege133d.xa ⊢ φ → X t+ ⁡ F A
3 frege133d.xb ⊢ φ → X t+ ⁡ F B
4 frege133d.fun ⊢ φ → Fun ⁡ F
5 funrel ⊢ Fun ⁡ F → Rel ⁡ F
6 4 5 syl ⊢ φ → Rel ⁡ F
7 reltrclfv ⊢ F ∈ V ∧ Rel ⁡ F → Rel ⁡ t+ ⁡ F
8 1 6 7 syl2anc ⊢ φ → Rel ⁡ t+ ⁡ F
9 eliniseg2 ⊢ Rel ⁡ t+ ⁡ F → X ∈ t+ ⁡ F -1 B ↔ X t+ ⁡ F B
10 8 9 syl ⊢ φ → X ∈ t+ ⁡ F -1 B ↔ X t+ ⁡ F B
11 3 10 mpbird ⊢ φ → X ∈ t+ ⁡ F -1 B
12 brrelex2 ⊢ Rel ⁡ t+ ⁡ F ∧ X t+ ⁡ F A → A ∈ V
13 8 2 12 syl2anc ⊢ φ → A ∈ V
14 un12 ⊢ t+ ⁡ F -1 B ∪ B ∪ t+ ⁡ F B = B ∪ t+ ⁡ F -1 B ∪ t+ ⁡ F B
15 14 a1i ⊢ φ → t+ ⁡ F -1 B ∪ B ∪ t+ ⁡ F B = B ∪ t+ ⁡ F -1 B ∪ t+ ⁡ F B
16 1 15 4 frege131d ⊢ φ → F t+ ⁡ F -1 B ∪ B ∪ t+ ⁡ F B ⊆ t+ ⁡ F -1 B ∪ B ∪ t+ ⁡ F B
17 1 11 13 2 16 frege83d ⊢ φ → A ∈ t+ ⁡ F -1 B ∪ B ∪ t+ ⁡ F B
18 elun ⊢ A ∈ B ∪ t+ ⁡ F B ↔ A ∈ B ∨ A ∈ t+ ⁡ F B
19 18 orbi2i ⊢ A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∪ t+ ⁡ F B ↔ A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∨ A ∈ t+ ⁡ F B
20 elun ⊢ A ∈ t+ ⁡ F -1 B ∪ B ∪ t+ ⁡ F B ↔ A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∪ t+ ⁡ F B
21 3orass ⊢ A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∨ A ∈ t+ ⁡ F B ↔ A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∨ A ∈ t+ ⁡ F B
22 19 20 21 3bitr4i ⊢ A ∈ t+ ⁡ F -1 B ∪ B ∪ t+ ⁡ F B ↔ A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∨ A ∈ t+ ⁡ F B
23 17 22 sylib ⊢ φ → A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∨ A ∈ t+ ⁡ F B
24 eliniseg2 ⊢ Rel ⁡ t+ ⁡ F → A ∈ t+ ⁡ F -1 B ↔ A t+ ⁡ F B
25 8 24 syl ⊢ φ → A ∈ t+ ⁡ F -1 B ↔ A t+ ⁡ F B
26 25 biimpd ⊢ φ → A ∈ t+ ⁡ F -1 B → A t+ ⁡ F B
27 elsni ⊢ A ∈ B → A = B
28 27 a1i ⊢ φ → A ∈ B → A = B
29 elrelimasn ⊢ Rel ⁡ t+ ⁡ F → A ∈ t+ ⁡ F B ↔ B t+ ⁡ F A
30 8 29 syl ⊢ φ → A ∈ t+ ⁡ F B ↔ B t+ ⁡ F A
31 30 biimpd ⊢ φ → A ∈ t+ ⁡ F B → B t+ ⁡ F A
32 26 28 31 3orim123d ⊢ φ → A ∈ t+ ⁡ F -1 B ∨ A ∈ B ∨ A ∈ t+ ⁡ F B → A t+ ⁡ F B ∨ A = B ∨ B t+ ⁡ F A
33 23 32 mpd ⊢ φ → A t+ ⁡ F B ∨ A = B ∨ B t+ ⁡ F A