Metamath Proof Explorer


Theorem weiunfr

Description: A well-founded relation on an indexed union can be constructed from a well-ordering on its index class and a collection of well-founded relations on its members. (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Hypotheses weiun.1 𝐹 = ( 𝑤 𝑥𝐴 𝐵 ↦ ( 𝑢 ∈ { 𝑥𝐴𝑤𝐵 } ∀ 𝑣 ∈ { 𝑥𝐴𝑤𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
weiun.2 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑦 ) 𝑅 ( 𝐹𝑧 ) ∨ ( ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ∧ 𝑦 ( 𝐹𝑦 ) / 𝑥 𝑆 𝑧 ) ) ) }
Assertion weiunfr ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) → 𝑇 Fr 𝑥𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 weiun.1 𝐹 = ( 𝑤 𝑥𝐴 𝐵 ↦ ( 𝑢 ∈ { 𝑥𝐴𝑤𝐵 } ∀ 𝑣 ∈ { 𝑥𝐴𝑤𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2 weiun.2 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑦 ) 𝑅 ( 𝐹𝑧 ) ∨ ( ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ∧ 𝑦 ( 𝐹𝑦 ) / 𝑥 𝑆 𝑧 ) ) ) }
3 csbeq1 ( 𝑠 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) → 𝑠 / 𝑥 𝑆 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 )
4 csbeq1 ( 𝑠 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) → 𝑠 / 𝑥 𝐵 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 )
5 3 4 freq12d ( 𝑠 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) → ( 𝑠 / 𝑥 𝑆 Fr 𝑠 / 𝑥 𝐵 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 Fr ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) )
6 simpl3 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ∀ 𝑥𝐴 𝑆 Fr 𝐵 )
7 nfv 𝑠 𝑆 Fr 𝐵
8 nfcsb1v 𝑥 𝑠 / 𝑥 𝑆
9 nfcsb1v 𝑥 𝑠 / 𝑥 𝐵
10 8 9 nffr 𝑥 𝑠 / 𝑥 𝑆 Fr 𝑠 / 𝑥 𝐵
11 csbeq1a ( 𝑥 = 𝑠𝑆 = 𝑠 / 𝑥 𝑆 )
12 csbeq1a ( 𝑥 = 𝑠𝐵 = 𝑠 / 𝑥 𝐵 )
13 11 12 freq12d ( 𝑥 = 𝑠 → ( 𝑆 Fr 𝐵 𝑠 / 𝑥 𝑆 Fr 𝑠 / 𝑥 𝐵 ) )
14 7 10 13 cbvralw ( ∀ 𝑥𝐴 𝑆 Fr 𝐵 ↔ ∀ 𝑠𝐴 𝑠 / 𝑥 𝑆 Fr 𝑠 / 𝑥 𝐵 )
15 6 14 sylib ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ∀ 𝑠𝐴 𝑠 / 𝑥 𝑆 Fr 𝑠 / 𝑥 𝐵 )
16 simpl1 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → 𝑅 We 𝐴 )
17 simpl2 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → 𝑅 Se 𝐴 )
18 1 2 16 17 weiunlem2 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝐹 : 𝑥𝐴 𝐵𝐴 ∧ ∀ 𝑡 𝑥𝐴 𝐵 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 ∧ ∀ 𝑠𝐴𝑡 𝑠 / 𝑥 𝐵 ¬ 𝑠 𝑅 ( 𝐹𝑡 ) ) )
19 18 simp1d ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → 𝐹 : 𝑥𝐴 𝐵𝐴 )
20 19 fimassd ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝐹𝑟 ) ⊆ 𝐴 )
21 eqid ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 )
22 simprl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → 𝑟 𝑥𝐴 𝐵 )
23 simprr ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → 𝑟 ≠ ∅ )
24 1 2 16 17 21 22 23 weiunfrlem ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∈ ( 𝐹𝑟 ) ∧ ∀ 𝑡𝑟 ¬ ( 𝐹𝑡 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∧ ∀ 𝑡 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) )
25 24 simp1d ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∈ ( 𝐹𝑟 ) )
26 20 25 sseldd ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∈ 𝐴 )
27 5 15 26 rspcdva ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 Fr ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 )
28 inss2 ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ⊆ ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵
29 28 a1i ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ⊆ ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 )
30 vex 𝑟 ∈ V
31 30 inex1 ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∈ V
32 31 a1i ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∈ V )
33 19 ffund ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → Fun 𝐹 )
34 fvelima ( ( Fun 𝐹 ∧ ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∈ ( 𝐹𝑟 ) ) → ∃ 𝑡𝑟 ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
35 33 25 34 syl2anc ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ∃ 𝑡𝑟 ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
36 simprl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → 𝑡𝑟 )
37 simplrl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → 𝑟 𝑥𝐴 𝐵 )
38 37 36 sseldd ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → 𝑡 𝑥𝐴 𝐵 )
39 18 simp2d ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ∀ 𝑡 𝑥𝐴 𝐵 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 )
40 39 r19.21bi ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ 𝑡 𝑥𝐴 𝐵 ) → 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 )
41 38 40 syldan ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 )
42 simprr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
43 42 csbeq1d ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → ( 𝐹𝑡 ) / 𝑥 𝐵 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 )
44 41 43 eleqtrd ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → 𝑡 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 )
45 36 44 elind ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → 𝑡 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) )
46 45 ne0d ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑡𝑟 ∧ ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) ) → ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ≠ ∅ )
47 35 46 rexlimddv ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ≠ ∅ )
48 27 29 32 47 frd ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ∃ 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 )
49 simprl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) → 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) )
50 49 elin1d ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) → 𝑛𝑟 )
51 fveq2 ( 𝑡 = 𝑜 → ( 𝐹𝑡 ) = ( 𝐹𝑜 ) )
52 51 breq1d ( 𝑡 = 𝑜 → ( ( 𝐹𝑡 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ↔ ( 𝐹𝑜 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) )
53 52 notbid ( 𝑡 = 𝑜 → ( ¬ ( 𝐹𝑡 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ↔ ¬ ( 𝐹𝑜 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) )
54 24 ad2antrr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ( ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∈ ( 𝐹𝑟 ) ∧ ∀ 𝑡𝑟 ¬ ( 𝐹𝑡 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∧ ∀ 𝑡 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) )
55 54 simp2d ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ∀ 𝑡𝑟 ¬ ( 𝐹𝑡 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
56 simpr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → 𝑜𝑟 )
57 53 55 56 rspcdva ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ¬ ( 𝐹𝑜 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
58 fveqeq2 ( 𝑡 = 𝑛 → ( ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ↔ ( 𝐹𝑛 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) )
59 54 simp3d ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ∀ 𝑡 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ( 𝐹𝑡 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
60 simplrl ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) )
61 58 59 60 rspcdva ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ( 𝐹𝑛 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
62 61 breq2d ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ( ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ↔ ( 𝐹𝑜 ) 𝑅 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ) )
63 57 62 mtbird ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ¬ ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) )
64 breq1 ( 𝑚 = 𝑜 → ( 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛𝑜 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) )
65 64 notbid ( 𝑚 = 𝑜 → ( ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ↔ ¬ 𝑜 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) )
66 simprr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) → ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 )
67 66 ad2antrr ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 )
68 simplr ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → 𝑜𝑟 )
69 id ( 𝑡 = 𝑜𝑡 = 𝑜 )
70 51 csbeq1d ( 𝑡 = 𝑜 ( 𝐹𝑡 ) / 𝑥 𝐵 = ( 𝐹𝑜 ) / 𝑥 𝐵 )
71 69 70 eleq12d ( 𝑡 = 𝑜 → ( 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵𝑜 ( 𝐹𝑜 ) / 𝑥 𝐵 ) )
72 39 ad3antrrr ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ∀ 𝑡 𝑥𝐴 𝐵 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 )
73 22 ad2antrr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → 𝑟 𝑥𝐴 𝐵 )
74 73 56 sseldd ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → 𝑜 𝑥𝐴 𝐵 )
75 74 adantr ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → 𝑜 𝑥𝐴 𝐵 )
76 71 72 75 rspcdva ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → 𝑜 ( 𝐹𝑜 ) / 𝑥 𝐵 )
77 simpr ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ( 𝐹𝑜 ) = ( 𝐹𝑛 ) )
78 61 adantr ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ( 𝐹𝑛 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
79 77 78 eqtrd ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ( 𝐹𝑜 ) = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
80 79 csbeq1d ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ( 𝐹𝑜 ) / 𝑥 𝐵 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 )
81 76 80 eleqtrd ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → 𝑜 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 )
82 68 81 elind ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → 𝑜 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) )
83 65 67 82 rspcdva ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ¬ 𝑜 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 )
84 79 csbeq1d ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ( 𝐹𝑜 ) / 𝑥 𝑆 = ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 )
85 84 breqd ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ( 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛𝑜 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) )
86 83 85 mtbird ( ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) ∧ ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ) → ¬ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 )
87 86 ex ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) → ¬ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) )
88 imnan ( ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) → ¬ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ↔ ¬ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) )
89 87 88 sylib ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ¬ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) )
90 pm4.56 ( ( ¬ ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ∧ ¬ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ) ↔ ¬ ( ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ∨ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ) )
91 90 biimpi ( ( ¬ ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ∧ ¬ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ) → ¬ ( ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ∨ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ) )
92 63 89 91 syl2anc ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ¬ ( ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ∨ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ) )
93 92 intnand ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ¬ ( ( 𝑜 𝑥𝐴 𝐵𝑛 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ∨ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ) ) )
94 1 2 weiunlem1 ( 𝑜 𝑇 𝑛 ↔ ( ( 𝑜 𝑥𝐴 𝐵𝑛 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑜 ) 𝑅 ( 𝐹𝑛 ) ∨ ( ( 𝐹𝑜 ) = ( 𝐹𝑛 ) ∧ 𝑜 ( 𝐹𝑜 ) / 𝑥 𝑆 𝑛 ) ) ) )
95 93 94 sylnibr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) ∧ 𝑜𝑟 ) → ¬ 𝑜 𝑇 𝑛 )
96 95 ralrimiva ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ∧ ∀ 𝑚 ∈ ( 𝑟 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝐵 ) ¬ 𝑚 ( 𝑝 ∈ ( 𝐹𝑟 ) ∀ 𝑞 ∈ ( 𝐹𝑟 ) ¬ 𝑞 𝑅 𝑝 ) / 𝑥 𝑆 𝑛 ) ) → ∀ 𝑜𝑟 ¬ 𝑜 𝑇 𝑛 )
97 48 50 96 reximssdv ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) ) → ∃ 𝑛𝑟𝑜𝑟 ¬ 𝑜 𝑇 𝑛 )
98 97 ex ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) → ( ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) → ∃ 𝑛𝑟𝑜𝑟 ¬ 𝑜 𝑇 𝑛 ) )
99 98 alrimiv ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) → ∀ 𝑟 ( ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) → ∃ 𝑛𝑟𝑜𝑟 ¬ 𝑜 𝑇 𝑛 ) )
100 df-fr ( 𝑇 Fr 𝑥𝐴 𝐵 ↔ ∀ 𝑟 ( ( 𝑟 𝑥𝐴 𝐵𝑟 ≠ ∅ ) → ∃ 𝑛𝑟𝑜𝑟 ¬ 𝑜 𝑇 𝑛 ) )
101 99 100 sylibr ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Fr 𝐵 ) → 𝑇 Fr 𝑥𝐴 𝐵 )