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 ( 𝑧 = ( 𝐹𝑥 ) → 𝑆 = 𝑈 )
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 𝐴 )