wsuclemOLD - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > wsuclemOLD		Structured version Visualization version GIF version

Theorem wsuclemOLD 31018

Description: Obsolete version of wsuclem 31017 as of 10-Oct-2021. (Contributed by Scott Fenton, 15-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

**Hypotheses**
Ref	Expression
wsuclem.1	⊢ (𝜑 → 𝑅 We 𝐴)
wsuclem.2	⊢ (𝜑 → 𝑅 Se 𝐴)
wsuclem.3	⊢ (𝜑 → 𝑋 ∈ 𝑉)
wsuclem.4	⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤)

**Assertion**
Ref	Expression
wsuclemOLD	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧)))

Distinct variable groups: 𝑥,𝐴,𝑦,𝑧,𝑤 𝜑,𝑥,𝑦 𝑥,𝑅,𝑦,𝑧,𝑤 𝑥,𝑋,𝑦,𝑧,𝑤 Allowed substitution hints: 𝜑(𝑧,𝑤) 𝑉(𝑥,𝑦,𝑧,𝑤)

**Proof of Theorem wsuclemOLD**
Step	Hyp	Ref	Expression
1		wsuclem.1	. . 3 ⊢ (𝜑 → 𝑅 We 𝐴)
2		wsuclem.2	. . 3 ⊢ (𝜑 → 𝑅 Se 𝐴)
3		predss 5604	. . . 4 ⊢ Pred(^◡𝑅, 𝐴, 𝑋) ⊆ 𝐴
4	3	a1i 11	. . 3 ⊢ (𝜑 → Pred(^◡𝑅, 𝐴, 𝑋) ⊆ 𝐴)
5		wsuclem.3	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
6		dfpred3g 5608	. . . . 5 ⊢ (𝑋 ∈ 𝑉 → Pred(^◡𝑅, 𝐴, 𝑋) = {𝑤 ∈ 𝐴 ∣ 𝑤^◡𝑅𝑋})
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → Pred(^◡𝑅, 𝐴, 𝑋) = {𝑤 ∈ 𝐴 ∣ 𝑤^◡𝑅𝑋})
8		elex 3185	. . . . . 6 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ V)
9	5, 8	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ V)
10		wsuclem.4	. . . . 5 ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤)
11		rabn0 3912	. . . . . . 7 ⊢ ({𝑤 ∈ 𝐴 ∣ 𝑤^◡𝑅𝑋} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 𝑤^◡𝑅𝑋)
12		brcnvg 5225	. . . . . . . . 9 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑋 ∈ V) → (𝑤^◡𝑅𝑋 ↔ 𝑋𝑅𝑤))
13	12	ancoms 468	. . . . . . . 8 ⊢ ((𝑋 ∈ V ∧ 𝑤 ∈ 𝐴) → (𝑤^◡𝑅𝑋 ↔ 𝑋𝑅𝑤))
14	13	rexbidva 3031	. . . . . . 7 ⊢ (𝑋 ∈ V → (∃𝑤 ∈ 𝐴 𝑤^◡𝑅𝑋 ↔ ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤))
15	11, 14	syl5bb 271	. . . . . 6 ⊢ (𝑋 ∈ V → ({𝑤 ∈ 𝐴 ∣ 𝑤^◡𝑅𝑋} ≠ ∅ ↔ ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤))
16	15	biimpar 501	. . . . 5 ⊢ ((𝑋 ∈ V ∧ ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) → {𝑤 ∈ 𝐴 ∣ 𝑤^◡𝑅𝑋} ≠ ∅)
17	9, 10, 16	syl2anc 691	. . . 4 ⊢ (𝜑 → {𝑤 ∈ 𝐴 ∣ 𝑤^◡𝑅𝑋} ≠ ∅)
18	7, 17	eqnetrd 2849	. . 3 ⊢ (𝜑 → Pred(^◡𝑅, 𝐴, 𝑋) ≠ ∅)
19		tz6.26 5628	. . 3 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (Pred(^◡𝑅, 𝐴, 𝑋) ⊆ 𝐴 ∧ Pred(^◡𝑅, 𝐴, 𝑋) ≠ ∅)) → ∃𝑥 ∈ Pred (^◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)
20	1, 2, 4, 18, 19	syl22anc 1319	. 2 ⊢ (𝜑 → ∃𝑥 ∈ Pred (^◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)
21		dfpred3g 5608	. . . . 5 ⊢ (𝑋 ∈ 𝑉 → Pred(^◡𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦^◡𝑅𝑋})
22	5, 21	syl 17	. . . 4 ⊢ (𝜑 → Pred(^◡𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦^◡𝑅𝑋})
23	22	rexeqdv 3122	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ Pred (^◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ ↔ ∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝑦^◡𝑅𝑋}Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅))
24		breq1 4586	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦^◡𝑅𝑋 ↔ 𝑥^◡𝑅𝑋))
25	24	rexrab 3337	. . . 4 ⊢ (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝑦^◡𝑅𝑋}Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ ↔ ∃𝑥 ∈ 𝐴 (𝑥^◡𝑅𝑋 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅))
26		noel 3878	. . . . . . . . . . . . 13 ⊢ ¬ 𝑦 ∈ ∅
27		simp2r 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)
28	27	eleq2d 2673	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → (𝑦 ∈ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) ↔ 𝑦 ∈ ∅))
29	26, 28	mtbiri 316	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → ¬ 𝑦 ∈ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥))
30		vex 3176	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
31	30	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → 𝑥 ∈ V)
32		simp3 1056	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋))
33		elpredg 5611	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → (𝑦 ∈ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) ↔ 𝑦𝑅𝑥))
34	31, 32, 33	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → (𝑦 ∈ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) ↔ 𝑦𝑅𝑥))
35	29, 34	mtbid 313	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → ¬ 𝑦𝑅𝑥)
36		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
37	30, 36	brcnv 5227	. . . . . . . . . . 11 ⊢ (𝑥^◡𝑅𝑦 ↔ 𝑦𝑅𝑥)
38	35, 37	sylnibr 318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → ¬ 𝑥^◡𝑅𝑦)
39	38	3expa 1257	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)) ∧ 𝑦 ∈ Pred(^◡𝑅, 𝐴, 𝑋)) → ¬ 𝑥^◡𝑅𝑦)
40	39	ralrimiva 2949	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅)) → ∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦)
41	40	expr 641	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ → ∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦))
42		simp1rl 1119	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → 𝑥 ∈ 𝐴)
43		simp1rr 1120	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → 𝑥^◡𝑅𝑋)
44		simp1l 1078	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → 𝜑)
45	44, 5	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → 𝑋 ∈ 𝑉)
46	30	elpred 5610	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑉 → (𝑥 ∈ Pred(^◡𝑅, 𝐴, 𝑋) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)))
47	45, 46	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → (𝑥 ∈ Pred(^◡𝑅, 𝐴, 𝑋) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)))
48	42, 43, 47	mpbir2and 959	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → 𝑥 ∈ Pred(^◡𝑅, 𝐴, 𝑋))
49		simp3 1056	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → 𝑦^◡𝑅𝑥)
50		breq2 4587	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑦^◡𝑅𝑧 ↔ 𝑦^◡𝑅𝑥))
51	50	rspcev 3282	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ Pred(^◡𝑅, 𝐴, 𝑋) ∧ 𝑦^◡𝑅𝑥) → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧)
52	48, 49, 51	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴 ∧ 𝑦^◡𝑅𝑥) → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧)
53	52	3expia 1259	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) ∧ 𝑦 ∈ 𝐴) → (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧))
54	53	ralrimiva 2949	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑥^◡𝑅𝑋)) → ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧))
55	54	expr 641	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥^◡𝑅𝑋 → ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧)))
56	41, 55	anim12d 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ ∧ 𝑥^◡𝑅𝑋) → (∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧))))
57	56	ancomsd 469	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥^◡𝑅𝑋 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) → (∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧))))
58	57	reximdva 3000	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 (𝑥^◡𝑅𝑋 ∧ Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧))))
59	25, 58	syl5bi 231	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝑦^◡𝑅𝑋}Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧))))
60	23, 59	sylbid 229	. 2 ⊢ (𝜑 → (∃𝑥 ∈ Pred (^◡𝑅, 𝐴, 𝑋)Pred(𝑅, Pred(^◡𝑅, 𝐴, 𝑋), 𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧))))
61	20, 60	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (^◡𝑅, 𝐴, 𝑋) ¬ 𝑥^◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦^◡𝑅𝑥 → ∃𝑧 ∈ Pred (^◡𝑅, 𝐴, 𝑋)𝑦^◡𝑅𝑧)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 Vcvv 3173 ⊆ wss 3540 ∅c0 3874 class class class wbr 4583 Se wse 4995 We wwe 4996 ^◡ccnv 5037 Predcpred 5596

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-cnv 5046 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597

This theorem is referenced by: (None)

W3C validator