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	weiunlem	⊢ ( ( ( 𝑅 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	weiunval	⊢ ( 𝑜 𝑇 𝑛 ↔ ( ( 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑛 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑜 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ∨ ( ( 𝐹 ‘ 𝑜 ) = ( 𝐹 ‘ 𝑛 ) ∧ 𝑜 ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝑆 𝑛 ) ) ) )
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 ∪ 𝑥 ∈ 𝐴 𝐵 )