Theorem weiunfrlem1

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

	Ref	Expression
Hypotheses	weiunfrlem1.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
	weiunfrlem1.2	⊢ 𝐶 = ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
Assertion	weiunfrlem1	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐶 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		weiunfrlem1.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		weiunfrlem1.2	⊢ 𝐶 = ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
3		simpl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) )
4	1	weiunlem1	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
5	4	adantr	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑤 ∈ ⦋ ( 𝐹 ‘ 𝑤 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑣 ∈ 𝐴 ( 𝑤 ∈ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 → ¬ 𝑣 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
6	5	simp1d	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
7	6	fimassd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐹 “ 𝑟 ) ⊆ 𝐴 )
8		simprl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
9	6	fdmd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → dom 𝐹 = ∪ 𝑥 ∈ 𝐴 𝐵 )
10	8 9	sseqtrrd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝑟 ⊆ dom 𝐹 )
11		sseqin2	⊢ ( 𝑟 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑟 ) = 𝑟 )
12	10 11	sylib	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( dom 𝐹 ∩ 𝑟 ) = 𝑟 )
13		simprr	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝑟 ≠ ∅ )
14	12 13	eqnetrd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( dom 𝐹 ∩ 𝑟 ) ≠ ∅ )
15	14	imadisjlnd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐹 “ 𝑟 ) ≠ ∅ )
16		wereu2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ( 𝐹 “ 𝑟 ) ⊆ 𝐴 ∧ ( 𝐹 “ 𝑟 ) ≠ ∅ ) ) → ∃! 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
17	3 7 15 16	syl12anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ∃! 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
18		riotacl2	⊢ ( ∃! 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 → ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 ) ∈ { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 } )
19	17 18	syl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 ) ∈ { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 } )
20	2 19	eqeltrid	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝐶 ∈ { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 } )
21	6	ffnd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵 )
22		breq1	⊢ ( 𝑡 = ( 𝐹 ‘ 𝑤 ) → ( 𝑡 𝑅 𝑠 ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 ) )
23	22	notbid	⊢ ( 𝑡 = ( 𝐹 ‘ 𝑤 ) → ( ¬ 𝑡 𝑅 𝑠 ↔ ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 ) )
24	23	ralima	⊢ ( ( 𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 ↔ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 ) )
25	24	rabbidv	⊢ ( ( 𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 } = { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 } )
26	21 8 25	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 } = { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 } )
27	20 26	eleqtrd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → 𝐶 ∈ { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 } )
28		nfriota1	⊢ Ⅎ 𝑠 ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
29	2 28	nfcxfr	⊢ Ⅎ 𝑠 𝐶
30		nfcv	⊢ Ⅎ 𝑠 ( 𝐹 “ 𝑟 )
31		nfcv	⊢ Ⅎ 𝑠 𝑟
32		nfcv	⊢ Ⅎ 𝑠 ( 𝐹 ‘ 𝑤 )
33		nfcv	⊢ Ⅎ 𝑠 𝑅
34	32 33 29	nfbr	⊢ Ⅎ 𝑠 ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶
35	34	nfn	⊢ Ⅎ 𝑠 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶
36	31 35	nfralw	⊢ Ⅎ 𝑠 ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶
37		breq2	⊢ ( 𝑠 = 𝐶 → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )
38	37	notbid	⊢ ( 𝑠 = 𝐶 → ( ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 ↔ ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )
39	38	ralbidv	⊢ ( 𝑠 = 𝐶 → ( ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 ↔ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )
40	29 30 36 39	elrabf	⊢ ( 𝐶 ∈ { 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑠 } ↔ ( 𝐶 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )
41	27 40	sylib	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅ ) ) → ( 𝐶 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑤 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑤 ) 𝑅 𝐶 ) )