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

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 imbitrid ⊢ ( ( ( 𝐹 ‘ 𝑏 ) = 𝑠 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑟 ) → ( 𝑏 = 𝑎 → 𝑠 = 𝑟 ) )
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 imbitrrdi ⊢ ( 𝑅 Po 𝐴 → ( ( ( 𝑤 We 𝐴 ∧ 𝑥 ∈ On ) ∧ ∀ 𝑦 ∈ 𝑥 𝐻 ≠ ∅ ) → 𝑅 Or ( 𝐹 “ 𝑥 ) ) )