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	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
	fnwe2.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
	fnwe2.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
	fnwe2.f	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 )
	fnwe2.r	⊢ ( 𝜑 → 𝑅 We 𝐵 )
Assertion	fnwe2	⊢ ( 𝜑 → 𝑇 We 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fnwe2.su	⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
2		fnwe2.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
3		fnwe2.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
4		fnwe2.f	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 )
5		fnwe2.r	⊢ ( 𝜑 → 𝑅 We 𝐵 )
6	3	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
7	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 )
8	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → 𝑅 We 𝐵 )
9		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → 𝑎 ⊆ 𝐴 )
10		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → 𝑎 ≠ ∅ )
11	1 2 6 7 8 9 10	fnwe2lem2	⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 )
12	11	ex	⊢ ( 𝜑 → ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 ) )
13	12	alrimiv	⊢ ( 𝜑 → ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 ) )
14		df-fr	⊢ ( 𝑇 Fr 𝐴 ↔ ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑎 ¬ 𝑑 𝑇 𝑐 ) )
15	13 14	sylibr	⊢ ( 𝜑 → 𝑇 Fr 𝐴 )
16	3	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
17	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 )
18	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑅 We 𝐵 )
19		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑎 ∈ 𝐴 )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 ∈ 𝐴 )
21	1 2 16 17 18 19 20	fnwe2lem3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) )
22	21	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) )
23		dfwe2	⊢ ( 𝑇 We 𝐴 ↔ ( 𝑇 Fr 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) ) )
24	15 22 23	sylanbrc	⊢ ( 𝜑 → 𝑇 We 𝐴 )

Metamath Proof Explorer

Theorem fnwe2

Proof