Users' Mathboxes Mathbox for Matthew House < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  weiunse Structured version   Visualization version   GIF version

Theorem weiunse 36383
Description: The relation constructed in weiunpo 36378, weiunso 36379, weiunfr 36382, and weiunwe 36384 is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025.)
Hypotheses
Ref Expression
weiunse.1 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
weiunse.2 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵) ∧ ((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)))}
Assertion
Ref Expression
weiunse ((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) → 𝑇 Se 𝑥𝐴 𝐵)
Distinct variable groups:   𝑢,𝐴,𝑣,𝑤,𝑥   𝑦,𝐴,𝑧,𝑥   𝑢,𝐵,𝑣,𝑤   𝑦,𝐵,𝑧   𝑦,𝐹,𝑧   𝑢,𝑅,𝑣,𝑤   𝑦,𝑅,𝑧   𝑦,𝑆,𝑧
Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥,𝑤,𝑣,𝑢)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐹(𝑥,𝑤,𝑣,𝑢)   𝑉(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)

Proof of Theorem weiunse
Dummy variables 𝑞 𝑠 𝑡 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl2 1192 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → 𝑅 Se 𝐴)
2 simpl1 1191 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → 𝑅 We 𝐴)
3 weiunse.1 . . . . . . . . . . 11 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
43weiunlem2 36377 . . . . . . . . . 10 ((𝑅 We 𝐴𝑅 Se 𝐴) → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑡 𝑥𝐴 𝐵𝑠𝐴 (𝑡𝑠 / 𝑥𝐵 → ¬ 𝑠𝑅(𝐹𝑡))))
52, 1, 4syl2anc 583 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑡 𝑥𝐴 𝐵𝑠𝐴 (𝑡𝑠 / 𝑥𝐵 → ¬ 𝑠𝑅(𝐹𝑡))))
65simp1d 1142 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → 𝐹: 𝑥𝐴 𝐵𝐴)
7 simpr 484 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → 𝑝 𝑥𝐴 𝐵)
86, 7ffvelcdmd 7117 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → (𝐹𝑝) ∈ 𝐴)
9 seex 5661 . . . . . . 7 ((𝑅 Se 𝐴 ∧ (𝐹𝑝) ∈ 𝐴) → {𝑟𝐴𝑟𝑅(𝐹𝑝)} ∈ V)
101, 8, 9syl2anc 583 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → {𝑟𝐴𝑟𝑅(𝐹𝑝)} ∈ V)
11 snex 5454 . . . . . 6 {(𝐹𝑝)} ∈ V
12 unexg 7774 . . . . . 6 (({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∈ V ∧ {(𝐹𝑝)} ∈ V) → ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}) ∈ V)
1310, 11, 12sylancl 585 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}) ∈ V)
14 ssrab2 4097 . . . . . . . 8 {𝑟𝐴𝑟𝑅(𝐹𝑝)} ⊆ 𝐴
1514a1i 11 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → {𝑟𝐴𝑟𝑅(𝐹𝑝)} ⊆ 𝐴)
168snssd 4834 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → {(𝐹𝑝)} ⊆ 𝐴)
1715, 16unssd 4209 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}) ⊆ 𝐴)
18 simpl3 1193 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → ∀𝑥𝐴 𝐵𝑉)
19 elex 3504 . . . . . . . . 9 (𝐵𝑉𝐵 ∈ V)
2019ralimi 3085 . . . . . . . 8 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
2118, 20syl 17 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → ∀𝑥𝐴 𝐵 ∈ V)
22 nfv 1913 . . . . . . . 8 𝑠 𝐵 ∈ V
23 nfcsb1v 3940 . . . . . . . . 9 𝑥𝑠 / 𝑥𝐵
2423nfel1 2921 . . . . . . . 8 𝑥𝑠 / 𝑥𝐵 ∈ V
25 csbeq1a 3929 . . . . . . . . 9 (𝑥 = 𝑠𝐵 = 𝑠 / 𝑥𝐵)
2625eleq1d 2823 . . . . . . . 8 (𝑥 = 𝑠 → (𝐵 ∈ V ↔ 𝑠 / 𝑥𝐵 ∈ V))
2722, 24, 26cbvralw 3307 . . . . . . 7 (∀𝑥𝐴 𝐵 ∈ V ↔ ∀𝑠𝐴 𝑠 / 𝑥𝐵 ∈ V)
2821, 27sylib 218 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → ∀𝑠𝐴 𝑠 / 𝑥𝐵 ∈ V)
29 ssralv 4071 . . . . . 6 (({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}) ⊆ 𝐴 → (∀𝑠𝐴 𝑠 / 𝑥𝐵 ∈ V → ∀𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵 ∈ V))
3017, 28, 29sylc 65 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → ∀𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵 ∈ V)
31 iunexg 8000 . . . . 5 ((({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}) ∈ V ∧ ∀𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵 ∈ V) → 𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵 ∈ V)
3213, 30, 31syl2anc 583 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → 𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵 ∈ V)
3363ad2ant1 1133 . . . . . . . . 9 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → 𝐹: 𝑥𝐴 𝐵𝐴)
34 simp2 1137 . . . . . . . . 9 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → 𝑞 𝑥𝐴 𝐵)
3533, 34ffvelcdmd 7117 . . . . . . . 8 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → (𝐹𝑞) ∈ 𝐴)
36 breq1 5172 . . . . . . . . . 10 (𝑟 = (𝐹𝑞) → (𝑟𝑅(𝐹𝑝) ↔ (𝐹𝑞)𝑅(𝐹𝑝)))
3736elrab 3703 . . . . . . . . 9 ((𝐹𝑞) ∈ {𝑟𝐴𝑟𝑅(𝐹𝑝)} ↔ ((𝐹𝑞) ∈ 𝐴 ∧ (𝐹𝑞)𝑅(𝐹𝑝)))
38 elun1 4199 . . . . . . . . 9 ((𝐹𝑞) ∈ {𝑟𝐴𝑟𝑅(𝐹𝑝)} → (𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}))
3937, 38sylbir 235 . . . . . . . 8 (((𝐹𝑞) ∈ 𝐴 ∧ (𝐹𝑞)𝑅(𝐹𝑝)) → (𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}))
4035, 39sylan 579 . . . . . . 7 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) ∧ (𝐹𝑞)𝑅(𝐹𝑝)) → (𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}))
41 fvex 6932 . . . . . . . . . 10 (𝐹𝑞) ∈ V
4241elsn 4663 . . . . . . . . 9 ((𝐹𝑞) ∈ {(𝐹𝑝)} ↔ (𝐹𝑞) = (𝐹𝑝))
43 elun2 4200 . . . . . . . . 9 ((𝐹𝑞) ∈ {(𝐹𝑝)} → (𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}))
4442, 43sylbir 235 . . . . . . . 8 ((𝐹𝑞) = (𝐹𝑝) → (𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}))
4544ad2antrl 727 . . . . . . 7 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) ∧ ((𝐹𝑞) = (𝐹𝑝) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑝)) → (𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}))
46 simpl 482 . . . . . . . . . . . . 13 ((𝑦 = 𝑞𝑧 = 𝑝) → 𝑦 = 𝑞)
4746fveq2d 6923 . . . . . . . . . . . 12 ((𝑦 = 𝑞𝑧 = 𝑝) → (𝐹𝑦) = (𝐹𝑞))
48 simpr 484 . . . . . . . . . . . . 13 ((𝑦 = 𝑞𝑧 = 𝑝) → 𝑧 = 𝑝)
4948fveq2d 6923 . . . . . . . . . . . 12 ((𝑦 = 𝑞𝑧 = 𝑝) → (𝐹𝑧) = (𝐹𝑝))
5047, 49breq12d 5182 . . . . . . . . . . 11 ((𝑦 = 𝑞𝑧 = 𝑝) → ((𝐹𝑦)𝑅(𝐹𝑧) ↔ (𝐹𝑞)𝑅(𝐹𝑝)))
5147, 49eqeq12d 2750 . . . . . . . . . . . 12 ((𝑦 = 𝑞𝑧 = 𝑝) → ((𝐹𝑦) = (𝐹𝑧) ↔ (𝐹𝑞) = (𝐹𝑝)))
5247csbeq1d 3919 . . . . . . . . . . . . 13 ((𝑦 = 𝑞𝑧 = 𝑝) → (𝐹𝑦) / 𝑥𝑆 = (𝐹𝑞) / 𝑥𝑆)
5346, 52, 48breq123d 5183 . . . . . . . . . . . 12 ((𝑦 = 𝑞𝑧 = 𝑝) → (𝑦(𝐹𝑦) / 𝑥𝑆𝑧𝑞(𝐹𝑞) / 𝑥𝑆𝑝))
5451, 53anbi12d 631 . . . . . . . . . . 11 ((𝑦 = 𝑞𝑧 = 𝑝) → (((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧) ↔ ((𝐹𝑞) = (𝐹𝑝) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑝)))
5550, 54orbi12d 917 . . . . . . . . . 10 ((𝑦 = 𝑞𝑧 = 𝑝) → (((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)) ↔ ((𝐹𝑞)𝑅(𝐹𝑝) ∨ ((𝐹𝑞) = (𝐹𝑝) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑝))))
56 weiunse.2 . . . . . . . . . 10 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵) ∧ ((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)))}
5755, 56brab2a 5792 . . . . . . . . 9 (𝑞𝑇𝑝 ↔ ((𝑞 𝑥𝐴 𝐵𝑝 𝑥𝐴 𝐵) ∧ ((𝐹𝑞)𝑅(𝐹𝑝) ∨ ((𝐹𝑞) = (𝐹𝑝) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑝))))
5857simprbi 496 . . . . . . . 8 (𝑞𝑇𝑝 → ((𝐹𝑞)𝑅(𝐹𝑝) ∨ ((𝐹𝑞) = (𝐹𝑝) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑝)))
59583ad2ant3 1135 . . . . . . 7 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → ((𝐹𝑞)𝑅(𝐹𝑝) ∨ ((𝐹𝑞) = (𝐹𝑝) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑝)))
6040, 45, 59mpjaodan 959 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → (𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}))
61 id 22 . . . . . . . 8 (𝑡 = 𝑞𝑡 = 𝑞)
62 fveq2 6919 . . . . . . . . 9 (𝑡 = 𝑞 → (𝐹𝑡) = (𝐹𝑞))
6362csbeq1d 3919 . . . . . . . 8 (𝑡 = 𝑞(𝐹𝑡) / 𝑥𝐵 = (𝐹𝑞) / 𝑥𝐵)
6461, 63eleq12d 2832 . . . . . . 7 (𝑡 = 𝑞 → (𝑡(𝐹𝑡) / 𝑥𝐵𝑞(𝐹𝑞) / 𝑥𝐵))
655simp2d 1143 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵)
66653ad2ant1 1133 . . . . . . 7 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵)
6764, 66, 34rspcdva 3632 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → 𝑞(𝐹𝑞) / 𝑥𝐵)
68 csbeq1 3918 . . . . . . 7 (𝑠 = (𝐹𝑞) → 𝑠 / 𝑥𝐵 = (𝐹𝑞) / 𝑥𝐵)
6968eliuni 5025 . . . . . 6 (((𝐹𝑞) ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)}) ∧ 𝑞(𝐹𝑞) / 𝑥𝐵) → 𝑞 𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵)
7060, 67, 69syl2anc 583 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) ∧ 𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝) → 𝑞 𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵)
7170rabssdv 4092 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → {𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝} ⊆ 𝑠 ∈ ({𝑟𝐴𝑟𝑅(𝐹𝑝)} ∪ {(𝐹𝑝)})𝑠 / 𝑥𝐵)
7232, 71ssexd 5345 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) ∧ 𝑝 𝑥𝐴 𝐵) → {𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝} ∈ V)
7372ralrimiva 3148 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) → ∀𝑝 𝑥𝐴 𝐵{𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝} ∈ V)
74 df-se 5655 . 2 (𝑇 Se 𝑥𝐴 𝐵 ↔ ∀𝑝 𝑥𝐴 𝐵{𝑞 𝑥𝐴 𝐵𝑞𝑇𝑝} ∈ V)
7573, 74sylibr 234 1 ((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝐵𝑉) → 𝑇 Se 𝑥𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 846  w3a 1087   = wceq 1537  wcel 2103  wral 3063  {crab 3438  Vcvv 3482  csb 3915  cun 3968  wss 3970  {csn 4648   ciun 5019   class class class wbr 5169  {copab 5231  cmpt 5252   Se wse 5652   We wwe 5653  wf 6568  cfv 6572  crio 7400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-rep 5306  ax-sep 5320  ax-nul 5327  ax-pr 5450  ax-un 7766
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-po 5611  df-so 5612  df-fr 5654  df-se 5655  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-fv 6580  df-riota 7401
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator