Metamath Proof Explorer

Theorem weiunfrlem2

Description: Lemma for weiunfr . (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Hypotheses weiunfrlem2.1 ⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
weiunfrlem2.2 ⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
weiunfrlem2.3 ⊢ 𝐶 = ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
Assertion weiunfrlem2 ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 weiunfrlem2.1 ⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2 weiunfrlem2.2 ⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
3 weiunfrlem2.3 ⊢ 𝐶 = ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
4 vex ⊢ 𝑟 ∈ V
5 4 inex1 ⊢ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∈ V
6 5 a1i ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∈ V )
7 1 weiunlem1 ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
8 7 adantr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
9 8 3adantl3 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
10 9 simp1d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
11 10 fimassd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐹 “ 𝑟 ) ⊆ 𝐴 )
12 1 3 weiunfrlem1 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐶 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )
13 12 3adantl3 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐶 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )
14 13 simpld ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝐶 ∈ ( 𝐹 “ 𝑟 ) )
15 11 14 sseldd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝐶 ∈ 𝐴 )
16 simpl3 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 )
17 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
18 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 }
19 nfv ⊢ Ⅎ 𝑥 ¬ 𝑣 𝑅 𝑢
20 18 19 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢
21 20 18 nfriota ⊢ Ⅎ 𝑥 ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 )
22 17 21 nfmpt ⊢ Ⅎ 𝑥 ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
23 1 22 nfcxfr ⊢ Ⅎ 𝑥 𝐹
24 nfcv ⊢ Ⅎ 𝑥 𝑟
25 23 24 nfima ⊢ Ⅎ 𝑥 ( 𝐹 “ 𝑟 )
26 nfv ⊢ Ⅎ 𝑥 ¬ 𝑡 𝑅 𝑠
27 25 26 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠
28 27 25 nfriota ⊢ Ⅎ 𝑥 ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
29 3 28 nfcxfr ⊢ Ⅎ 𝑥 𝐶
30 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵
31 29 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ 𝐶 / 𝑥 ⦌ 𝑆
32 29 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ 𝐶 / 𝑥 ⦌ 𝐵
33 31 32 nffr ⊢ Ⅎ 𝑥 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵
34 30 33 nfim ⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
35 csbeq1a ⊢ ( 𝑥 = 𝐶 → 𝑆 = ⦋ 𝐶 / 𝑥 ⦌ 𝑆 )
36 freq1 ⊢ ( 𝑆 = ⦋ 𝐶 / 𝑥 ⦌ 𝑆 → ( 𝑆 Fr 𝐵 ↔ ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr 𝐵 ) )
37 35 36 syl ⊢ ( 𝑥 = 𝐶 → ( 𝑆 Fr 𝐵 ↔ ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr 𝐵 ) )
38 csbeq1a ⊢ ( 𝑥 = 𝐶 → 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
39 freq2 ⊢ ( 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 → ( ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr 𝐵 ↔ ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
40 38 39 syl ⊢ ( 𝑥 = 𝐶 → ( ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr 𝐵 ↔ ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
41 37 40 bitrd ⊢ ( 𝑥 = 𝐶 → ( 𝑆 Fr 𝐵 ↔ ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
42 41 imbi2d ⊢ ( 𝑥 = 𝐶 → ( ( ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → 𝑆 Fr 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ) )
43 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑆 Fr 𝐵 ) )
44 43 com12 ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → 𝑆 Fr 𝐵 ) )
45 29 34 42 44 vtoclgaf ⊢ ( 𝐶 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
46 15 16 45 sylc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
47 inss2 ⊢ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ⊆ ⦋ 𝐶 / 𝑥 ⦌ 𝐵
48 47 a1i ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ⊆ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
49 10 ffund ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → Fun 𝐹 )
50 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝐶 ∈ ( 𝐹 “ 𝑟 ) ) → ∃ 𝑜 ∈ 𝑟 ( 𝐹 ‘ 𝑜 ) = 𝐶 )
51 49 14 50 syl2anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ∃ 𝑜 ∈ 𝑟 ( 𝐹 ‘ 𝑜 ) = 𝐶 )
52 simprl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → 𝑜 ∈ 𝑟 )
53 simplrl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
54 53 52 sseldd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
55 9 simp2d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 )
56 55 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 )
57 id ⊢ ( 𝑤 = 𝑜 → 𝑤 = 𝑜 )
58 fveq2 ⊢ ( 𝑤 = 𝑜 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑜 ) )
59 58 csbeq1d ⊢ ( 𝑤 = 𝑜 → ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝐵 )
60 57 59 eleq12d ⊢ ( 𝑤 = 𝑜 → ( 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ↔ 𝑜 ∈ ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝐵 ) )
61 60 rspcv ⊢ ( 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ( ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 → 𝑜 ∈ ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝐵 ) )
62 54 56 61 sylc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → 𝑜 ∈ ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝐵 )
63 csbeq1 ⊢ ( ( 𝐹 ‘ 𝑜 ) = 𝐶 → ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
64 63 ad2antll ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
65 62 64 eleqtrd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → 𝑜 ∈ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
66 52 65 elind ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → 𝑜 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
67 66 ne0d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑜 ∈ 𝑟 ∧ ( 𝐹 ‘ 𝑜 ) = 𝐶 ) ) → ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ≠ ∅ )
68 51 67 rexlimddv ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ≠ ∅ )
69 fri ⊢ ( ( ( ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∈ V ∧ ⦋ 𝐶 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ( ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ⊆ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ∧ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ≠ ∅ ) ) → ∃ 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 )
70 6 46 48 68 69 syl22anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ∃ 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 )
71 simprl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
72 71 elin1d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝑝 ∈ 𝑟 )
73 13 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( 𝐶 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )
74 73 simprd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 )
75 fveq2 ⊢ ( 𝑤 = 𝑡 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑡 ) )
76 75 breq1d ⊢ ( 𝑤 = 𝑡 → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ↔ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐶 ) )
77 76 notbid ⊢ ( 𝑤 = 𝑡 → ( ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ↔ ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐶 ) )
78 77 rspcv ⊢ ( 𝑡 ∈ 𝑟 → ( ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 → ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐶 ) )
79 74 78 mpan9 ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐶 )
80 fveq2 ⊢ ( 𝑤 = 𝑝 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑝 ) )
81 80 breq1d ⊢ ( 𝑤 = 𝑝 → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ↔ ( 𝐹 ‘ 𝑝 ) 𝑅 𝐶 ) )
82 81 notbid ⊢ ( 𝑤 = 𝑝 → ( ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ↔ ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 𝐶 ) )
83 82 rspcv ⊢ ( 𝑝 ∈ 𝑟 → ( ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 → ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 𝐶 ) )
84 72 74 83 sylc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 𝐶 )
85 9 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
86 85 simp3d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
87 71 elin2d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝑝 ∈ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
88 simplrl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
89 88 72 sseldd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
90 15 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝐶 ∈ 𝐴 )
91 simpl ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → 𝑤 = 𝑝 )
92 simpr ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → 𝑣 = 𝐶 )
93 92 csbeq1d ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → ⦋ 𝑣 / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
94 91 93 eleq12d ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ↔ 𝑝 ∈ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
95 91 fveq2d ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑝 ) )
96 92 95 breq12d ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → ( 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ↔ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) ) )
97 96 notbid ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → ( ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ↔ ¬ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) ) )
98 94 97 imbi12d ⊢ ( ( 𝑤 = 𝑝 ∧ 𝑣 = 𝐶 ) → ( ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑝 ∈ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 → ¬ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) ) ) )
99 98 rspc2gv ⊢ ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) → ( 𝑝 ∈ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 → ¬ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) ) ) )
100 89 90 99 syl2anc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) → ( 𝑝 ∈ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 → ¬ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) ) ) )
101 86 87 100 mp2d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ¬ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) )
102 simpll1 ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝑅 We 𝐴 )
103 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
104 102 103 syl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝑅 Or 𝐴 )
105 10 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
106 105 89 ffvelcdmd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 )
107 sotrieq2 ⊢ ( ( 𝑅 Or 𝐴 ∧ ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑝 ) = 𝐶 ↔ ( ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 𝐶 ∧ ¬ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) ) ) )
108 104 106 90 107 syl12anc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( ( 𝐹 ‘ 𝑝 ) = 𝐶 ↔ ( ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 𝐶 ∧ ¬ 𝐶 𝑅 ( 𝐹 ‘ 𝑝 ) ) ) )
109 84 101 108 mpbir2and ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( 𝐹 ‘ 𝑝 ) = 𝐶 )
110 109 adantr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ( 𝐹 ‘ 𝑝 ) = 𝐶 )
111 breq2 ⊢ ( ( 𝐹 ‘ 𝑝 ) = 𝐶 → ( ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐶 ) )
112 111 notbid ⊢ ( ( 𝐹 ‘ 𝑝 ) = 𝐶 → ( ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐶 ) )
113 110 112 syl ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ( ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐶 ) )
114 79 113 mpbird ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) )
115 simplr ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → 𝑡 ∈ 𝑟 )
116 88 sselda ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
117 55 ad2antrr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 )
118 id ⊢ ( 𝑤 = 𝑡 → 𝑤 = 𝑡 )
119 75 csbeq1d ⊢ ( 𝑤 = 𝑡 → ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
120 118 119 eleq12d ⊢ ( 𝑤 = 𝑡 → ( 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ↔ 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ) )
121 120 rspcv ⊢ ( 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ( ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 → 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ) )
122 116 117 121 sylc ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
123 122 adantr ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
124 simpr ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) )
125 110 adantr ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑝 ) = 𝐶 )
126 124 125 eqtrd ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑡 ) = 𝐶 )
127 126 csbeq1d ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
128 123 127 eleqtrd ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → 𝑡 ∈ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
129 115 128 elind ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
130 simprr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 )
131 130 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 )
132 breq1 ⊢ ( 𝑞 = 𝑡 → ( 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ↔ 𝑡 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) )
133 132 notbid ⊢ ( 𝑞 = 𝑡 → ( ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ↔ ¬ 𝑡 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) )
134 133 rspcv ⊢ ( 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) → ( ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 → ¬ 𝑡 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) )
135 129 131 134 sylc ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ¬ 𝑡 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 )
136 126 csbeq1d ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 = ⦋ 𝐶 / 𝑥 ⦌ 𝑆 )
137 136 breqd ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ( 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ↔ 𝑡 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) )
138 135 137 mtbird ⊢ ( ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) ∧ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) → ¬ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 )
139 138 ex ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) → ¬ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) )
140 imnan ⊢ ( ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) → ¬ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ↔ ¬ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) )
141 139 140 sylib ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ¬ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) )
142 pm4.56 ⊢ ( ( ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∧ ¬ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ↔ ¬ ( ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
143 142 biimpi ⊢ ( ( ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∧ ¬ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) → ¬ ( ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
144 114 141 143 syl2anc ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ¬ ( ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
145 144 intnand ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ¬ ( ( 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
146 simpl ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → 𝑦 = 𝑡 )
147 146 fveq2d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑡 ) )
148 simpr ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → 𝑧 = 𝑝 )
149 148 fveq2d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑝 ) )
150 147 149 breq12d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) )
151 147 149 eqeq12d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ) )
152 147 csbeq1d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 )
153 146 152 148 breq123d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) )
154 151 153 anbi12d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
155 150 154 orbi12d ⊢ ( ( 𝑦 = 𝑡 ∧ 𝑧 = 𝑝 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
156 155 2 brab2a ⊢ ( 𝑡 𝑇 𝑝 ↔ ( ( 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑡 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑡 ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
157 145 156 sylnibr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) ∧ 𝑡 ∈ 𝑟 ) → ¬ 𝑡 𝑇 𝑝 )
158 157 ralrimiva ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) ∧ ( 𝑝 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∧ ∀ 𝑞 ∈ ( 𝑟 ∩ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ¬ 𝑞 ⦋ 𝐶 / 𝑥 ⦌ 𝑆 𝑝 ) ) → ∀ 𝑡 ∈ 𝑟 ¬ 𝑡 𝑇 𝑝 )
159 70 72 158 reximssdv ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ∃ 𝑝 ∈ 𝑟 ∀ 𝑡 ∈ 𝑟 ¬ 𝑡 𝑇 𝑝 )
160 159 ex ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) → ( ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑟 ∀ 𝑡 ∈ 𝑟 ¬ 𝑡 𝑇 𝑝 ) )
161 160 alrimiv ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) → ∀ 𝑟 ( ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑟 ∀ 𝑡 ∈ 𝑟 ¬ 𝑡 𝑇 𝑝 ) )
162 df-fr ⊢ ( 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑟 ( ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) → ∃ 𝑝 ∈ 𝑟 ∀ 𝑡 ∈ 𝑟 ¬ 𝑡 𝑇 𝑝 ) )
163 161 162 sylibr ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 )