This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnwe2

Description: A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su ⊢ z = F ⁡ x → S = U
fnwe2.t ⊢ T = x y | F ⁡ x R F ⁡ y ∨ F ⁡ x = F ⁡ y ∧ x U y
fnwe2.s ⊢ φ ∧ x ∈ A → U We y ∈ A | F ⁡ y = F ⁡ x
fnwe2.f ⊢ φ → F ↾ A : A ⟶ B
fnwe2.r ⊢ φ → R We B
Assertion fnwe2 ⊢ φ → T We A

Proof

Step Hyp Ref Expression
1 fnwe2.su ⊢ z = F ⁡ x → S = U
2 fnwe2.t ⊢ T = x y | F ⁡ x R F ⁡ y ∨ F ⁡ x = F ⁡ y ∧ x U y
3 fnwe2.s ⊢ φ ∧ x ∈ A → U We y ∈ A | F ⁡ y = F ⁡ x
4 fnwe2.f ⊢ φ → F ↾ A : A ⟶ B
5 fnwe2.r ⊢ φ → R We B
6 3 adantlr ⊢ φ ∧ a ⊆ A ∧ a ≠ ∅ ∧ x ∈ A → U We y ∈ A | F ⁡ y = F ⁡ x
7 4 adantr ⊢ φ ∧ a ⊆ A ∧ a ≠ ∅ → F ↾ A : A ⟶ B
8 5 adantr ⊢ φ ∧ a ⊆ A ∧ a ≠ ∅ → R We B
9 simprl ⊢ φ ∧ a ⊆ A ∧ a ≠ ∅ → a ⊆ A
10 simprr ⊢ φ ∧ a ⊆ A ∧ a ≠ ∅ → a ≠ ∅
11 1 2 6 7 8 9 10 fnwe2lem2 ⊢ φ ∧ a ⊆ A ∧ a ≠ ∅ → ∃ c ∈ a ∀ d ∈ a ¬ d T c
12 11 ex ⊢ φ → a ⊆ A ∧ a ≠ ∅ → ∃ c ∈ a ∀ d ∈ a ¬ d T c
13 12 alrimiv ⊢ φ → ∀ a a ⊆ A ∧ a ≠ ∅ → ∃ c ∈ a ∀ d ∈ a ¬ d T c
14 df-fr ⊢ T Fr A ↔ ∀ a a ⊆ A ∧ a ≠ ∅ → ∃ c ∈ a ∀ d ∈ a ¬ d T c
15 13 14 sylibr ⊢ φ → T Fr A
16 3 adantlr ⊢ φ ∧ a ∈ A ∧ b ∈ A ∧ x ∈ A → U We y ∈ A | F ⁡ y = F ⁡ x
17 4 adantr ⊢ φ ∧ a ∈ A ∧ b ∈ A → F ↾ A : A ⟶ B
18 5 adantr ⊢ φ ∧ a ∈ A ∧ b ∈ A → R We B
19 simprl ⊢ φ ∧ a ∈ A ∧ b ∈ A → a ∈ A
20 simprr ⊢ φ ∧ a ∈ A ∧ b ∈ A → b ∈ A
21 1 2 16 17 18 19 20 fnwe2lem3 ⊢ φ ∧ a ∈ A ∧ b ∈ A → a T b ∨ a = b ∨ b T a
22 21 ralrimivva ⊢ φ → ∀ a ∈ A ∀ b ∈ A a T b ∨ a = b ∨ b T a
23 dfwe2 ⊢ T We A ↔ T Fr A ∧ ∀ a ∈ A ∀ b ∈ A a T b ∨ a = b ∨ b T a
24 15 22 23 sylanbrc ⊢ φ → T We A