Metamath Proof Explorer


Theorem zorn2lem6

Description: Lemma for zorn2 . (Contributed by NM, 4-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses zorn2lem.3 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
zorn2lem.4 𝐶 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
zorn2lem.5 𝐷 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑥 ) 𝑔 𝑅 𝑧 }
zorn2lem.7 𝐻 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 }
Assertion zorn2lem6 ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → 𝑅 Or ( 𝐹𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 zorn2lem.3 𝐹 = recs ( ( 𝑓 ∈ V ↦ ( 𝑣𝐶𝑢𝐶 ¬ 𝑢 𝑤 𝑣 ) ) )
2 zorn2lem.4 𝐶 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ran 𝑓 𝑔 𝑅 𝑧 }
3 zorn2lem.5 𝐷 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑥 ) 𝑔 𝑅 𝑧 }
4 zorn2lem.7 𝐻 = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 }
5 poss ( ( 𝐹𝑥 ) ⊆ 𝐴 → ( 𝑅 Po 𝐴𝑅 Po ( 𝐹𝑥 ) ) )
6 1 2 3 4 zorn2lem5 ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → ( 𝐹𝑥 ) ⊆ 𝐴 )
7 5 6 syl11 ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → 𝑅 Po ( 𝐹𝑥 ) ) )
8 1 tfr1 𝐹 Fn On
9 fnfun ( 𝐹 Fn On → Fun 𝐹 )
10 fvelima ( ( Fun 𝐹𝑠 ∈ ( 𝐹𝑥 ) ) → ∃ 𝑏𝑥 ( 𝐹𝑏 ) = 𝑠 )
11 df-rex ( ∃ 𝑏𝑥 ( 𝐹𝑏 ) = 𝑠 ↔ ∃ 𝑏 ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) )
12 10 11 sylib ( ( Fun 𝐹𝑠 ∈ ( 𝐹𝑥 ) ) → ∃ 𝑏 ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) )
13 12 ex ( Fun 𝐹 → ( 𝑠 ∈ ( 𝐹𝑥 ) → ∃ 𝑏 ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ) )
14 fvelima ( ( Fun 𝐹𝑟 ∈ ( 𝐹𝑥 ) ) → ∃ 𝑎𝑥 ( 𝐹𝑎 ) = 𝑟 )
15 df-rex ( ∃ 𝑎𝑥 ( 𝐹𝑎 ) = 𝑟 ↔ ∃ 𝑎 ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) )
16 14 15 sylib ( ( Fun 𝐹𝑟 ∈ ( 𝐹𝑥 ) ) → ∃ 𝑎 ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) )
17 16 ex ( Fun 𝐹 → ( 𝑟 ∈ ( 𝐹𝑥 ) → ∃ 𝑎 ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) )
18 13 17 anim12d ( Fun 𝐹 → ( ( 𝑠 ∈ ( 𝐹𝑥 ) ∧ 𝑟 ∈ ( 𝐹𝑥 ) ) → ( ∃ 𝑏 ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ∧ ∃ 𝑎 ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) ) )
19 8 9 18 mp2b ( ( 𝑠 ∈ ( 𝐹𝑥 ) ∧ 𝑟 ∈ ( 𝐹𝑥 ) ) → ( ∃ 𝑏 ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ∧ ∃ 𝑎 ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) )
20 an4 ( ( ( 𝑏𝑥𝑎𝑥 ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) ↔ ( ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ∧ ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) )
21 20 2exbii ( ∃ 𝑏𝑎 ( ( 𝑏𝑥𝑎𝑥 ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) ↔ ∃ 𝑏𝑎 ( ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ∧ ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) )
22 exdistrv ( ∃ 𝑏𝑎 ( ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ∧ ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) ↔ ( ∃ 𝑏 ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ∧ ∃ 𝑎 ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) )
23 21 22 bitri ( ∃ 𝑏𝑎 ( ( 𝑏𝑥𝑎𝑥 ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) ↔ ( ∃ 𝑏 ( 𝑏𝑥 ∧ ( 𝐹𝑏 ) = 𝑠 ) ∧ ∃ 𝑎 ( 𝑎𝑥 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) )
24 19 23 sylibr ( ( 𝑠 ∈ ( 𝐹𝑥 ) ∧ 𝑟 ∈ ( 𝐹𝑥 ) ) → ∃ 𝑏𝑎 ( ( 𝑏𝑥𝑎𝑥 ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) )
25 4 neeq1i ( 𝐻 ≠ ∅ ↔ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } ≠ ∅ )
26 25 ralbii ( ∀ 𝑦𝑥 𝐻 ≠ ∅ ↔ ∀ 𝑦𝑥 { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } ≠ ∅ )
27 imaeq2 ( 𝑦 = 𝑏 → ( 𝐹𝑦 ) = ( 𝐹𝑏 ) )
28 27 raleqdv ( 𝑦 = 𝑏 → ( ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 ) )
29 28 rabbidv ( 𝑦 = 𝑏 → { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } )
30 29 neeq1d ( 𝑦 = 𝑏 → ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } ≠ ∅ ↔ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) )
31 30 rspccv ( ∀ 𝑦𝑥 { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } ≠ ∅ → ( 𝑏𝑥 → { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) )
32 imaeq2 ( 𝑦 = 𝑎 → ( 𝐹𝑦 ) = ( 𝐹𝑎 ) )
33 32 raleqdv ( 𝑦 = 𝑎 → ( ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 ↔ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 ) )
34 33 rabbidv ( 𝑦 = 𝑎 → { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } )
35 34 neeq1d ( 𝑦 = 𝑎 → ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } ≠ ∅ ↔ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) )
36 35 rspccv ( ∀ 𝑦𝑥 { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } ≠ ∅ → ( 𝑎𝑥 → { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) )
37 31 36 anim12d ( ∀ 𝑦𝑥 { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑦 ) 𝑔 𝑅 𝑧 } ≠ ∅ → ( ( 𝑏𝑥𝑎𝑥 ) → ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) )
38 26 37 sylbi ( ∀ 𝑦𝑥 𝐻 ≠ ∅ → ( ( 𝑏𝑥𝑎𝑥 ) → ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) )
39 onelon ( ( 𝑥 ∈ On ∧ 𝑏𝑥 ) → 𝑏 ∈ On )
40 onelon ( ( 𝑥 ∈ On ∧ 𝑎𝑥 ) → 𝑎 ∈ On )
41 39 40 anim12dan ( ( 𝑥 ∈ On ∧ ( 𝑏𝑥𝑎𝑥 ) ) → ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) )
42 41 ex ( 𝑥 ∈ On → ( ( 𝑏𝑥𝑎𝑥 ) → ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ) )
43 eloni ( 𝑏 ∈ On → Ord 𝑏 )
44 eloni ( 𝑎 ∈ On → Ord 𝑎 )
45 ordtri3or ( ( Ord 𝑏 ∧ Ord 𝑎 ) → ( 𝑏𝑎𝑏 = 𝑎𝑎𝑏 ) )
46 43 44 45 syl2an ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑏𝑎𝑏 = 𝑎𝑎𝑏 ) )
47 eqid { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 }
48 1 2 47 zorn2lem2 ( ( 𝑎 ∈ On ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( 𝑏𝑎 → ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ) )
49 48 adantll ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( 𝑏𝑎 → ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ) )
50 breq12 ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ↔ 𝑠 𝑅 𝑟 ) )
51 50 biimpcd ( ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → 𝑠 𝑅 𝑟 ) )
52 49 51 syl6 ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( 𝑏𝑎 → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → 𝑠 𝑅 𝑟 ) ) )
53 52 com23 ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑏𝑎𝑠 𝑅 𝑟 ) ) )
54 53 adantrrl ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑏𝑎𝑠 𝑅 𝑟 ) ) )
55 54 imp ( ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) → ( 𝑏𝑎𝑠 𝑅 𝑟 ) )
56 fveq2 ( 𝑏 = 𝑎 → ( 𝐹𝑏 ) = ( 𝐹𝑎 ) )
57 eqeq12 ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( ( 𝐹𝑏 ) = ( 𝐹𝑎 ) ↔ 𝑠 = 𝑟 ) )
58 56 57 syl5ib ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑏 = 𝑎𝑠 = 𝑟 ) )
59 58 adantl ( ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) → ( 𝑏 = 𝑎𝑠 = 𝑟 ) )
60 eqid { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } = { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 }
61 1 2 60 zorn2lem2 ( ( 𝑏 ∈ On ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( 𝑎𝑏 → ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ) )
62 61 adantlr ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( 𝑎𝑏 → ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ) )
63 breq12 ( ( ( 𝐹𝑎 ) = 𝑟 ∧ ( 𝐹𝑏 ) = 𝑠 ) → ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ↔ 𝑟 𝑅 𝑠 ) )
64 63 ancoms ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ↔ 𝑟 𝑅 𝑠 ) )
65 64 biimpcd ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → 𝑟 𝑅 𝑠 ) )
66 62 65 syl6 ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( 𝑎𝑏 → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → 𝑟 𝑅 𝑠 ) ) )
67 66 com23 ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑎𝑏𝑟 𝑅 𝑠 ) ) )
68 67 adantrrr ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑎𝑏𝑟 𝑅 𝑠 ) ) )
69 68 imp ( ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) → ( 𝑎𝑏𝑟 𝑅 𝑠 ) )
70 55 59 69 3orim123d ( ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) → ( ( 𝑏𝑎𝑏 = 𝑎𝑎𝑏 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) )
71 46 70 syl5 ( ( ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) ∧ ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) → ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) )
72 71 exp31 ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) )
73 72 com4r ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( ( 𝑏 ∈ On ∧ 𝑎 ∈ On ) → ( ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) )
74 42 42 73 syl6c ( 𝑥 ∈ On → ( ( 𝑏𝑥𝑎𝑥 ) → ( ( 𝑤 We 𝐴 ∧ ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) )
75 74 exp4a ( 𝑥 ∈ On → ( ( 𝑏𝑥𝑎𝑥 ) → ( 𝑤 We 𝐴 → ( ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) ) )
76 75 com3r ( 𝑤 We 𝐴 → ( 𝑥 ∈ On → ( ( 𝑏𝑥𝑎𝑥 ) → ( ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) ) )
77 76 imp ( ( 𝑤 We 𝐴𝑥 ∈ On ) → ( ( 𝑏𝑥𝑎𝑥 ) → ( ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) )
78 77 a2d ( ( 𝑤 We 𝐴𝑥 ∈ On ) → ( ( ( 𝑏𝑥𝑎𝑥 ) → ( { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑏 ) 𝑔 𝑅 𝑧 } ≠ ∅ ∧ { 𝑧𝐴 ∣ ∀ 𝑔 ∈ ( 𝐹𝑎 ) 𝑔 𝑅 𝑧 } ≠ ∅ ) ) → ( ( 𝑏𝑥𝑎𝑥 ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) )
79 38 78 syl5 ( ( 𝑤 We 𝐴𝑥 ∈ On ) → ( ∀ 𝑦𝑥 𝐻 ≠ ∅ → ( ( 𝑏𝑥𝑎𝑥 ) → ( ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) ) )
80 79 imp4b ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → ( ( ( 𝑏𝑥𝑎𝑥 ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) )
81 80 exlimdvv ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → ( ∃ 𝑏𝑎 ( ( 𝑏𝑥𝑎𝑥 ) ∧ ( ( 𝐹𝑏 ) = 𝑠 ∧ ( 𝐹𝑎 ) = 𝑟 ) ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) )
82 24 81 syl5 ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → ( ( 𝑠 ∈ ( 𝐹𝑥 ) ∧ 𝑟 ∈ ( 𝐹𝑥 ) ) → ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) )
83 82 ralrimivv ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → ∀ 𝑠 ∈ ( 𝐹𝑥 ) ∀ 𝑟 ∈ ( 𝐹𝑥 ) ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) )
84 7 83 jca2 ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → ( 𝑅 Po ( 𝐹𝑥 ) ∧ ∀ 𝑠 ∈ ( 𝐹𝑥 ) ∀ 𝑟 ∈ ( 𝐹𝑥 ) ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) ) )
85 df-so ( 𝑅 Or ( 𝐹𝑥 ) ↔ ( 𝑅 Po ( 𝐹𝑥 ) ∧ ∀ 𝑠 ∈ ( 𝐹𝑥 ) ∀ 𝑟 ∈ ( 𝐹𝑥 ) ( 𝑠 𝑅 𝑟𝑠 = 𝑟𝑟 𝑅 𝑠 ) ) )
86 84 85 syl6ibr ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴𝑥 ∈ On ) ∧ ∀ 𝑦𝑥 𝐻 ≠ ∅ ) → 𝑅 Or ( 𝐹𝑥 ) ) )